Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∨ wo 846
= wceq 1542 ∈
wcel 2107 suc csuc 6367 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3954 df-sn 4630 df-suc 6371 |
This theorem is referenced by: suctr
6451 pssnn
9168 pssnnOLD
9265 ttrcltr
9711 ttrclss
9715 ttrclselem2
9721 pwsdompw
10199 fin1a2lem4
10398 grur1a
10814 bnj570
33916 satom
34347 satfv0
34349 satfvsuc
34352 satf00
34365 satf0suc
34367 sat1el2xp
34370 fmla
34372 fmla0
34373 fmlasuc0
34375 satfdmfmla
34391 finxpsuclem
36278 |