![]() |
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 4881 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴) | |
2 | 1 | eleq1d 2823 | . 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V)) |
3 | vuniex 7681 | . 2 ⊢ ∪ 𝑥 ∈ V | |
4 | 2, 3 | vtoclg 3528 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 Vcvv 3448 ∪ cuni 4870 |
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-un 7677 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-in 3922 df-ss 3932 df-uni 4871 |
This theorem is referenced by: uniex 7683 uniexd 7684 abnexg 7695 uniexb 7703 pwexr 7704 ssonuni 7719 ssonprc 7727 dmexg 7845 rnexg 7846 undefval 8212 onovuni 8293 tz7.44lem1 8356 tz7.44-3 8359 en1unielOLD 8980 disjen 9085 domss2 9087 fival 9355 fipwuni 9369 supexd 9396 cantnflem1 9632 dfac8clem 9975 onssnum 9983 dfac12lem1 10086 dfac12lem2 10087 fin1a2lem12 10354 hsmexlem1 10369 wrdexb 14420 restid 17322 prdsbas 17346 prdsplusg 17347 prdsmulr 17348 prdsvsca 17349 prdshom 17356 sscpwex 17705 pmtrfv 19241 istopon 22277 tgval 22321 eltg2 22324 tgss2 22353 neiptoptop 22498 restin 22533 restntr 22549 cnprest2 22657 pnrmopn 22710 cnrmnrm 22728 cmpsublem 22766 cmpsub 22767 cmpcld 22769 hausmapdom 22867 isref 22876 locfindis 22897 txbasex 22933 dfac14lem 22984 xkopt 23022 xkopjcn 23023 qtopval2 23063 elqtop 23064 fbssfi 23204 ptcmplem2 23420 cnextfval 23429 tuslem 23634 tuslemOLD 23635 madeval 27204 pliguhgr 29470 acunirnmpt2 31618 acunirnmpt2f 31619 ist0cld 32454 hasheuni 32724 insiga 32776 sigagenval 32779 omsval 32933 omssubadd 32940 sibfof 32980 sitmcl 32991 kur14 33850 cvmscld 33907 fobigcup 34514 hfuni 34798 isfne 34840 isfne4b 34842 fnemeet1 34867 tailfval 34873 bj-restuni2 35598 pibt2 35917 imaexALTV 36820 kelac2 41421 cnfex 43307 unidmex 43332 pwpwuni 43339 salgenval 44636 intsaluni 44644 salgenn0 44646 caragenunidm 44823 afv2ex 45520 iscnrm3rlem3 47049 |
Copyright terms: Public domain | W3C validator |