Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
∈ wcel 2107 ⊆
wss 3914 Tr wtr 5226
Ord word 6320 |
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-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3062 df-v 3449 df-in 3921 df-ss 3931 df-uni 4870 df-tr 5227 df-ord 6324 |
This theorem is referenced by: onfr
6360 onelss
6363 ordtri2or2
6420 onfununi
8291 smores3
8303 tfrlem1
8326 tfrlem9a
8336 tz7.44-2
8357 tz7.44-3
8358 oaabslem
8597 oaabs2
8599 omabslem
8600 omabs
8601 findcard3
9235 findcard3OLD
9236 nnsdomg
9252 nnsdomgOLD
9253 ordiso2
9459 ordtypelem2
9463 ordtypelem6
9467 ordtypelem7
9468 cantnf
9637 cnfcomlem
9643 ttrcltr
9660 cardmin2
9943 infxpenlem
9957 iunfictbso
10058 dfac12lem2
10088 dfac12lem3
10089 unctb
10149 ackbij2lem1
10163 ackbij1lem3
10166 ackbij1lem18
10181 ackbij2
10187 ttukeylem6
10458 ttukeylem7
10459 alephexp1
10523 fpwwe2lem7
10581 pwfseqlem3
10604 pwdjundom
10611 fz1isolem
14369 noinfbday
27091 onsuct0
34966 finxpreclem4
35915 nadd2rabtr
41747 grur1cld
42604 |