Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∨ wo 843
= wceq 1539 ∈
wcel 2104 suc csuc 6365 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2701 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-or 844 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-v 3474 df-un 3952 df-sn 4628 df-suc 6369 |
This theorem is referenced by: suctr
6449 pssnn
9170 pssnnOLD
9267 ttrcltr
9713 ttrclss
9717 ttrclselem2
9723 pwsdompw
10201 fin1a2lem4
10400 grur1a
10816 bnj570
34214 satom
34645 satfv0
34647 satfvsuc
34650 satf00
34663 satf0suc
34665 sat1el2xp
34668 fmla
34670 fmla0
34671 fmlasuc0
34673 satfdmfmla
34689 finxpsuclem
36581 |