![]() |
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 4747 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴) | |
2 | 1 | eleq1d 2865 | . 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V)) |
3 | vuniex 7315 | . 2 ⊢ ∪ 𝑥 ∈ V | |
4 | 2, 3 | vtoclg 3505 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1520 ∈ wcel 2079 Vcvv 3432 ∪ cuni 4739 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-ext 2767 ax-sep 5088 ax-un 7310 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-rex 3109 df-v 3434 df-uni 4740 |
This theorem is referenced by: abnexg 7326 uniexb 7334 pwexr 7335 ssonuni 7348 ssonprc 7354 dmexg 7460 rnexg 7461 iunexg 7511 undefval 7784 onovuni 7822 tz7.44lem1 7884 tz7.44-3 7887 en1b 8415 en1uniel 8419 disjen 8511 domss2 8513 fival 8712 fipwuni 8726 supexd 8753 cantnflem1 8987 dfac8clem 9293 onssnum 9301 dfac12lem1 9404 dfac12lem2 9405 fin1a2lem12 9668 hsmexlem1 9683 axdc2lem 9705 ttukeylem3 9768 wrdexb 13707 restid 16524 prdsbas 16547 prdsplusg 16548 prdsmulr 16549 prdsvsca 16550 prdshom 16557 sscpwex 16902 pmtrfv 18299 frgpcyg 20390 istopon 21192 tgval 21235 eltg 21237 eltg2 21238 tgss2 21267 ntrval 21316 neiptoptop 21411 neiptopnei 21412 restin 21446 neitr 21460 restntr 21462 cnpresti 21568 cnprest 21569 cnprest2 21570 lmcnp 21584 pnrmopn 21623 cnrmnrm 21641 cmpsublem 21679 cmpsub 21680 cmpcld 21682 hausmapdom 21780 isref 21789 locfindis 21810 txbasex 21846 dfac14lem 21897 uptx 21905 xkopt 21935 xkopjcn 21936 qtopval2 21976 elqtop 21977 fbssfi 22117 ptcmplem2 22333 cnextfval 22342 cnextcn 22347 tuslem 22547 isppw 25361 pliguhgr 27942 elpwunicl 29975 acunirnmpt2 30068 acunirnmpt2f 30069 hasheuni 30917 insiga 30969 sigagenval 30972 braew 31074 omsval 31124 omssubaddlem 31130 omssubadd 31131 omsmeas 31154 sibfof 31171 sitmcl 31182 isrrvv 31274 rrvmulc 31284 bnj1489 31898 kur14 32027 cvmscld 32084 bdayimaon 32751 nosupno 32757 madeval 32843 fobigcup 32915 hfuni 33199 isfne 33241 isfne4b 33243 topjoin 33267 fnemeet1 33268 tailfval 33274 bj-restuni2 33934 pibt2 34175 mbfresfi 34415 supex2g 34490 imaexALTV 35068 kelac2 39101 cnfex 40776 unidmex 40803 pwpwuni 40810 uniexd 40859 unirnmap 40964 stoweidlem50 41831 stoweidlem57 41838 stoweidlem59 41840 stoweidlem60 41841 fourierdlem71 41958 salgenval 42102 intsaluni 42108 intsal 42109 salgenn0 42110 caragenval 42271 omecl 42281 caragenunidm 42286 afv2ex 42883 setrec1lem2 44225 |
Copyright terms: Public domain | W3C validator |