equ
Top-level context.
Equality and Substitution
Theorems:
Name
Comment
aleqcom
ax10b
ax10ex
ax16-bv
ax17-bv
ax17eq
ax4a
ax4c
ax4c1
ax9-sv
ax9alt
ax9alt-sv
ax9ex
bi.bldsb
bi.bldsbd
bi.bldsbt
bv-distvar
bv-idvar
bv-sb-d1
bv-sbb-dv
cbv1
cbv2
cbv3
cbval
cbval2
cbvald
cbvex
cbvex2
cbvexd
chvar
chvar-∀
chvar-∀-1w
chvar-∀-w
chvar-∃
dfsb-alt
dfsb-dval
dfsb-dvex
dfsbf
dral1
dral2
drex1
drex2
dveeq1
ee4anv
eeanv
eq-sb>b
eqcomi
eqid
eqs3lem
eqs4lem
eqs5lem
eqsal
eqsex
eqt-sb
eqt-sbi
eqtr
eqvin
eqvini
eqvini-sv
exan<vv
exan>vv
exan>vvv
exdistr
exdistr2
im.bldsb
im.bldsbt
naleqcoms
sb-an
sb-bi
sb-bi<
sb-bi>
sb-bv
sb-bvw
sb-eqat<
sb-eqat<w
sb-eqat<x
sb-eqat<xw
sb-eqat>
sb-im
sb-neg
sb-negw
sb-or
sb-orw
sb-spec-ex
sb-xpl
sb-xplw
sbal
sbal-w
sbco2
sbco2w
sbex
sbid
spec
spec-w
Subcontexts:
Name
Comment
eq
equiv-ax-=
Axioms for equivalence relations