Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uniexg | Structured version Visualization version GIF version |
Description: The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to make the theorem more general and thus shorten some proofs; obviously the universal class constant V is one possible substitution for class variable 𝑉. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
uniexg | ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unieq 4380 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴) | |
2 | 1 | eleq1d 2672 | . 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V)) |
3 | vuniex 6852 | . 2 ⊢ ∪ 𝑥 ∈ V | |
4 | 2, 3 | vtoclg 3239 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 Vcvv 3173 ∪ cuni 4372 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-un 6847 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-v 3175 df-uni 4373 |
This theorem is referenced by: snnex 6862 uniexb 6866 ssonuni 6878 ssonprc 6884 dmexg 6989 rnexg 6990 iunexg 7035 undefval 7289 onovuni 7326 tz7.44lem1 7388 tz7.44-3 7391 en1b 7910 en1uniel 7914 disjen 8002 domss2 8004 fival 8201 fipwuni 8215 supexd 8242 cantnflem1 8469 dfac8clem 8738 onssnum 8746 dfac12lem1 8848 dfac12lem2 8849 fin1a2lem12 9116 hsmexlem1 9131 axdc2lem 9153 ttukeylem3 9216 wrdexb 13171 restid 15917 prdsbas 15940 prdsplusg 15941 prdsmulr 15942 prdsvsca 15943 prdshom 15950 sscpwex 16298 pmtrfv 17695 frgpcyg 19741 istopon 20540 tgval 20570 eltg 20572 eltg2 20573 tgss2 20602 ntrval 20650 neiptoptop 20745 neiptopnei 20746 restin 20780 neitr 20794 restntr 20796 cnpresti 20902 cnprest 20903 cnprest2 20904 lmcnp 20918 pnrmopn 20957 cnrmnrm 20975 cmpsublem 21012 cmpsub 21013 cmpcld 21015 hausmapdom 21113 isref 21122 locfindis 21143 txbasex 21179 dfac14lem 21230 uptx 21238 xkopt 21268 xkopjcn 21269 qtopval2 21309 elqtop 21310 fbssfi 21451 ptcmplem2 21667 cnextfval 21676 cnextcn 21681 tuslem 21881 isppw 24640 elpwunicl 28754 acunirnmpt2 28842 acunirnmpt2f 28843 hasheuni 29474 insiga 29527 sigagenval 29530 braew 29632 omsval 29682 omssubaddlem 29688 omssubadd 29689 omsmeas 29712 sibfof 29729 sitmcl 29740 isrrvv 29832 rrvmulc 29842 bnj1489 30378 kur14 30452 cvmscld 30509 nobndlem1 31091 fobigcup 31177 hfuni 31461 isfne 31504 isfne4b 31506 topjoin 31530 fnemeet1 31531 tailfval 31537 bj-restuni2 32232 bj-xnex 32245 mbfresfi 32626 supex2g 32702 kelac2 36653 cnfex 38210 unidmex 38242 pwpwuni 38250 uniexd 38310 unirnmap 38395 stoweidlem50 38943 stoweidlem57 38950 stoweidlem59 38952 stoweidlem60 38953 fourierdlem71 39070 salgenval 39217 intsaluni 39223 intsal 39224 salgenn0 39225 caragenval 39383 omecl 39393 caragenunidm 39398 setrec1lem2 42234 |
Copyright terms: Public domain | W3C validator |