Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
∈ wcel 2107 Vcvv 3448
∪ cun 3913 |
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 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 ax-un 7677 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-sn 4592 df-pr 4594 df-uni 4871 |
This theorem is referenced by: xpexg
7689 unexd
7693 difex2
7699 difsnexi
7700 eldifpw
7707 pwuncl
7709 ordunpr
7766 soex
7863 fnse
8070 suppun
8120 tposexg
8176 frrlem13
8234 wfrlem15OLD
8274 tfrlem12
8340 tfrlem16
8344 elmapresaun
8825 ralxpmap
8841 undifixp
8879 undom
9010 undomOLD
9011 domunsncan
9023 domssex2
9088 domssex
9089 mapunen
9097 sbthfilem
9152 fsuppunbi
9333 elfiun
9373 brwdom2
9516 unwdomg
9527 djuex
9851 djuexALT
9865 alephprc
10042 djudoml
10127 infunabs
10150 fin23lem11
10260 axdc2lem
10391 ttukeylem1
10452 fpwwe2lem12
10585 wunex2
10681 wuncval2
10690 hashunx
14293 hashf1lem1
14360 hashf1lem1OLD
14361 trclexlem
14886 trclun
14906 relexp0g
14914 relexpsucnnr
14917 isstruct2
17028 setsvalg
17045 setsid
17087 yonffth
18180 pwmndgplus
18752 dmdprdsplit2
19832 basdif0
22319 fiuncmp
22771 refun0
22882 ptbasfi
22948 dfac14lem
22984 ptrescn
23006 xkoptsub
23021 filconn
23250 isufil2
23275 ufileu
23286 filufint
23287 fmfnfmlem4
23324 fmfnfm
23325 fclsfnflim
23394 flimfnfcls
23395 ptcmplem1
23419 elply2
25573 plyss
25576 noeta2
27146 etasslt2
27175 scutbdaybnd2lim
27178 wlkp1lem4
28666 resf1o
31689 tocycfv
32000 tocycf
32008 locfinref
32462 esumsplit
32692 esumpad2
32695 sseqval
33028 bnj1149
33444 satfvsuc
33995 satf0suclem
34009 sat1el2xp
34013 fmlasuc0
34018 altxpexg
34592 hfun
34792 refssfne
34859 topjoin
34866 bj-2uplex
35522 ptrest
36106 poimirlem3
36110 paddval
38290 elrfi
41046 rtrclexlem
41962 clcnvlem
41969 cnvrcl0
41971 dfrtrcl5
41975 iunrelexp0
42048 relexpxpmin
42063 brtrclfv2
42073 sge0resplit
44721 sge0split
44724 setsv
45644 setrec1lem4
47209 |