Colors of
variables: wff setvar class |
Syntax hints: wn 3
wb 176
wal 1540
wex 1541
wceq 1642
wcel 1710
cvv 2860
c0 3551
csn 3738 |
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-sn 4088 |
This theorem depends on definitions:
df-bi 177 df-or 359
df-an 360 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-v 2862 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-ss 3260 df-nul 3552 df-sn 3742 |
This theorem is referenced by: prex
4113 snelpwg
4115 snelpwi
4117 sspwb
4119 pwadjoin
4120 elopk
4130 el1c
4140 elpw1
4145 elpw12
4146 elpw11c
4148 elpw121c
4149 elpw131c
4150 elpw141c
4151 elpw151c
4152 elpw161c
4153 elpw171c
4154 elpw181c
4155 elpw191c
4156 elpw1101c
4157 elpw1111c
4158 eqpw1
4163 pw111
4171 eluni1g
4173 otkelins2kg
4254 otkelins3kg
4255 opkelcokg
4262 elp6
4264 opksnelsik
4266 elssetkg
4270 opkelimagekg
4272 ins2kss
4280 ins3kss
4281 dfuni12
4292 sikexlem
4296 sikexg
4297 dfimak2
4299 insklem
4305 ins2kexg
4306 ins3kexg
4307 dfuni3
4316 dfint3
4319 setswith
4322 setswithex
4323 ndisjrelk
4324 unipw1
4326 dfpw2
4328 dfaddc2
4382 0cex
4393 dfnnc2
4396 nnc0suc
4413 elsuc
4414 nnsucelrlem1
4425 nnsucelr
4429 nndisjeq
4430 preaddccan2lem1
4455 ltfinex
4465 ltfintrilem1
4466 ssfin
4471 ncfinsn
4477 eqpwrelk
4479 eqpw1relk
4480 ncfinraiselem2
4481 ncfinraise
4482 ncfinlowerlem1
4483 ncfinlower
4484 eqtfinrelk
4487 tfinrelkex
4488 tfinsuc
4499 evenfinex
4504 oddfinex
4505 evenoddnnnul
4515 evenodddisjlem1
4516 nnadjoinlem1
4520 nnadjoin
4521 nnadjoinpw
4522 nnpweqlem1
4523 srelk
4525 sfindbl
4531 sfintfinlem1
4532 tfinnnlem1
4534 spfinex
4538 vfinspnn
4542 vfinspss
4552 vfinspclt
4553 vfinncsp
4555 nulnnn
4557 dfop2lem1
4574 opexg
4588 proj2exg
4593 proj2op
4602 phiall
4619 setconslem1
4732 setconslem2
4733 setconslem3
4734 setconslem4
4735 setconslem5
4736 setconslem6
4737 setconslem7
4738 df1st2
4739 1stex
4740 dfswap2
4742 swapex
4743 brssetsn
4760 brsi
4762 elimapw1
4945 elimapw12
4946 elimapw13
4947 elimapw11c
4949 elxp4
5109 dmsi
5520 dmep
5525 brsnsi
5774 brimage
5794 composeex
5821 addcfnex
5825 funsex
5829 crossex
5851 pw1fnex
5853 pw1fnf1o
5856 fullfunexg
5860 domfnex
5871 ranfnex
5872 clos1ex
5877 transex
5911 refex
5912 antisymex
5913 connexex
5914 foundex
5915 extex
5916 symex
5917 ecexg
5950 qsexg
5983 mapexi
6004 map0
6026 mapsn
6027 en2sn
6048 xpsnen
6050 endisj
6052 xpsnen2g
6055 enadj
6061 enpw1lem1
6062 enmap2lem1
6064 enmap1lem1
6070 enpw1pw
6076 enprmaplem1
6077 enprmaplem2
6078 enprmaplem3
6079 enprmaplem5
6081 enprmaplem6
6082 nenpw1pwlem1
6085 lecex
6116 mucex
6134 1cnc
6140 mucid1
6144 ncaddccl
6145 1p1e2c
6156 2p1e3c
6157 tcdi
6165 tc1c
6166 ovcelem1
6172 ceexlem1
6174 ceex
6175 ce0addcnnul
6180 ce0nn
6181 el2c
6192 ce2
6193 leconnnc
6219 tcfnex
6245 0lt1c
6259 csucex
6260 addccan2nclem2
6265 nmembers1lem1
6269 nncdiv3lem2
6277 nnc3n3p1
6279 spacvallem1
6282 spacval
6283 fnspac
6284 spacssnc
6285 spacind
6288 nchoicelem3
6292 nchoicelem4
6293 nchoicelem6
6295 nchoicelem7
6296 nchoicelem10
6299 nchoicelem11
6300 nchoicelem14
6303 nchoicelem16
6305 nchoicelem18
6307 frecexg
6313 frecxp
6315 dmfrec
6317 fnfreclem2
6319 fnfreclem3
6320 frec0
6322 frecsuc
6323 dmsnfn
6328 scancan
6332 |