Colors of
variables: wff
setvar class |
Syntax hints: -> wi 4 = wceq 1395
e. wcel 1818 A. wral 2807 C_ wss 3475
Tr wtr 4545 |
This theorem is referenced by: trin
4555 triun
4558 trint0
4562 tz7.2
4868 ordelss
4899 ordelord
4905 tz7.7
4909 trsucss
4968 tc2
8194 tcel
8197 r1ord3g
8218 r1ord2
8220 r1pwss
8223 rankwflemb
8232 r1elwf
8235 r1elssi
8244 uniwf
8258 itunitc1
8821 wunelss
9107 tskr1om2
9167 tskuni
9182 tskurn
9188 gruelss
9193 dfon2lem6
29220 dfon2lem9
29223 omsinds
29299 setindtr
30966 dford3lem1
30968 ordelordALT
33308 trsspwALT
33616 trsspwALT2
33617 trsspwALT3
33618 pwtrVD
33624 ordelordALTVD
33667 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704
ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions:
df-bi 185 df-an 371
df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ral 2812 df-v 3111 df-in 3482 df-ss 3489 df-uni 4250 df-tr 4546 |