![]() |
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 4596 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴) | |
2 | 1 | eleq1d 2824 | . 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V)) |
3 | vuniex 7119 | . 2 ⊢ ∪ 𝑥 ∈ V | |
4 | 2, 3 | vtoclg 3406 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1632 ∈ wcel 2139 Vcvv 3340 ∪ cuni 4588 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-un 7114 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-rex 3056 df-v 3342 df-uni 4589 |
This theorem is referenced by: abnexg 7129 snnexOLD 7132 uniexb 7138 pwexr 7139 ssonuni 7151 ssonprc 7157 dmexg 7262 rnexg 7263 iunexg 7308 undefval 7571 onovuni 7608 tz7.44lem1 7670 tz7.44-3 7673 en1b 8189 en1uniel 8193 disjen 8282 domss2 8284 fival 8483 fipwuni 8497 supexd 8524 cantnflem1 8759 dfac8clem 9045 onssnum 9053 dfac12lem1 9157 dfac12lem2 9158 fin1a2lem12 9425 hsmexlem1 9440 axdc2lem 9462 ttukeylem3 9525 wrdexb 13502 restid 16296 prdsbas 16319 prdsplusg 16320 prdsmulr 16321 prdsvsca 16322 prdshom 16329 sscpwex 16676 pmtrfv 18072 frgpcyg 20124 istopon 20919 tgval 20961 eltg 20963 eltg2 20964 tgss2 20993 ntrval 21042 neiptoptop 21137 neiptopnei 21138 restin 21172 neitr 21186 restntr 21188 cnpresti 21294 cnprest 21295 cnprest2 21296 lmcnp 21310 pnrmopn 21349 cnrmnrm 21367 cmpsublem 21404 cmpsub 21405 cmpcld 21407 hausmapdom 21505 isref 21514 locfindis 21535 txbasex 21571 dfac14lem 21622 uptx 21630 xkopt 21660 xkopjcn 21661 qtopval2 21701 elqtop 21702 fbssfi 21842 ptcmplem2 22058 cnextfval 22067 cnextcn 22072 tuslem 22272 isppw 25039 pliguhgr 27649 elpwunicl 29678 acunirnmpt2 29769 acunirnmpt2f 29770 hasheuni 30456 insiga 30509 sigagenval 30512 braew 30614 omsval 30664 omssubaddlem 30670 omssubadd 30671 omsmeas 30694 sibfof 30711 sitmcl 30722 isrrvv 30814 rrvmulc 30824 bnj1489 31431 kur14 31505 cvmscld 31562 bdayimaon 32149 nosupno 32155 madeval 32241 fobigcup 32313 hfuni 32597 isfne 32640 isfne4b 32642 topjoin 32666 fnemeet1 32667 tailfval 32673 bj-restuni2 33357 mbfresfi 33769 supex2g 33845 kelac2 38137 cnfex 39686 unidmex 39716 pwpwuni 39724 uniexd 39780 unirnmap 39899 stoweidlem50 40770 stoweidlem57 40777 stoweidlem59 40779 stoweidlem60 40780 fourierdlem71 40897 salgenval 41044 intsaluni 41050 intsal 41051 salgenn0 41052 caragenval 41213 omecl 41223 caragenunidm 41228 setrec1lem2 42945 |
Copyright terms: Public domain | W3C validator |