Colors of
variables: wff setvar class |
Syntax hints: →
wi 4 ↔ wb 176
= wceq 1642 ∈ wcel 1710 ⟨cop 4562 class class class wbr 4640 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675
ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 ax-sn 4088 |
This theorem depends on definitions:
df-bi 177 df-or 359
df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-idk 4196 df-addc 4379 df-nnc 4380 df-phi 4566 df-op 4567 df-br 4641 |
This theorem is referenced by: breq12
4645 breq1i
4647 breq1d
4650 nbrne2
4658 brab1
4685 vtoclr
4817 brco
4884 brcnv
4893 dfdmf
4906 elimapw1
4945 dfrnf
4963 dfres2
5003 imasn
5019 coi1
5095 dffun6f
5124 funmo
5126 fun11
5160 fneu
5188 fveq2
5329 nfunsn
5354 dmfco
5382 dff13
5472 isorel
5490 isocnv
5492 isotr
5496 isomin
5497 isoini
5498 f1oiso
5500 f1oiso2
5501 funsi
5521 caovord
5630 caovord3
5632 brsnsi
5774 brsnsi1
5776 brco1st
5778 brco2nd
5779 trtxp
5782 elfix
5788 op1st2nd
5791 brimage
5794 txpcofun
5804 otsnelsi3
5806 addcfnex
5825 qrpprod
5837 brpprod
5840 dmpprod
5841 fnpprod
5844 clos1ex
5877 clos1conn
5880 clos1basesuc
5883 trd
5922 symd
5925 antid
5930 connexd
5932 weds
5939 en0
6043 fndmeng
6047 endisj
6052 xpassenlem
6057 xpassen
6058 enpw1
6063 enmap2
6069 enpw1pw
6076 nenpw1pwlem2
6086 enpw
6088 lecex
6116 ovmuc
6131 mucnc
6132 mucex
6134 ncdisjun
6137 ceexlem1
6174 ceex
6175 elce
6176 ltlenlec
6208 leltctr
6213 leconnnc
6219 lenc
6224 ce2le
6234 ce0lenc1
6240 tcfnex
6245 nclenn
6250 csucex
6260 addccan2nclem1
6264 ncslesuc
6268 nmembers1lem1
6269 nmembers1lem3
6271 nncdiv3lem1
6276 nncdiv3lem2
6277 nnc3n3p1
6279 spacvallem1
6282 nchoicelem11
6300 nchoicelem16
6305 nchoicelem19
6308 fnfreclem3
6320 fnfrec
6321 frecsuc
6323 |