Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 class class class wbr 5109
≈ cen 8886 ≼
cdom 8887 |
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-10 2138 ax-12 2172 ax-ext 2704 ax-sep 5260 ax-nul 5267 ax-pr 5388 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-br 5110 df-opab 5172 df-xp 5643 df-rel 5644 df-f1o 6507 df-en 8890 df-dom 8891 |
This theorem is referenced by: bren2
8929 domrefg
8933 endomtr
8958 domentr
8959 domunsncan
9022 sbthb
9044 dom0
9052 sdomentr
9061 ensdomtr
9063 domtriord
9073 domunsn
9077 xpen
9090 sdomdomtrfi
9154 domsdomtrfi
9155 sucdom2
9156 php
9160 php3
9162 onomeneq
9178 0sdom1dom
9188 rex2dom
9196 unxpdom2
9204 sucxpdom
9205 f1finf1o
9221 findcard3
9235 wdomen1
9520 wdomen2
9521 fidomtri2
9938 prdom2
9950 acnen
9997 acnen2
9999 alephdom
10025 alephinit
10039 undjudom
10111 pwdjudom
10160 fin1a2lem11
10354 hsmexlem1
10370 gchdomtri
10573 gchdjuidm
10612 gchxpidm
10613 gchpwdom
10614 gchhar
10623 gruina
10762 nnct
13895 odinf
19353 hauspwdom
22875 ufildom1
23300 iscmet3
24680 mbfaddlem
25047 ctbssinf
35927 pibt2
35938 heiborlem3
36322 zct
43361 qct
43687 caratheodory
44859 |