![]() |
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 4923 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴) | |
2 | 1 | eleq1d 2810 | . 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V)) |
3 | vuniex 7749 | . 2 ⊢ ∪ 𝑥 ∈ V | |
4 | 2, 3 | vtoclg 3533 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 Vcvv 3461 ∪ cuni 4912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5303 ax-un 7745 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-ss 3963 df-uni 4913 |
This theorem is referenced by: uniex 7751 uniexd 7752 abnexg 7763 uniexb 7771 pwexr 7772 ssonuni 7787 ssonprc 7795 dmexg 7913 rnexg 7914 undefval 8290 onovuni 8371 tz7.44lem1 8434 tz7.44-3 8437 en1unielOLD 9064 disjen 9171 domss2 9173 fival 9451 fipwuni 9465 supexd 9492 cantnflem1 9728 dfac8clem 10071 onssnum 10079 dfac12lem1 10182 dfac12lem2 10183 fin1a2lem12 10450 hsmexlem1 10465 wrdexb 14528 restid 17443 prdsbas 17467 prdsplusg 17468 prdsmulr 17469 prdsvsca 17470 prdshom 17477 sscpwex 17826 pmtrfv 19445 istopon 22897 tgval 22941 eltg2 22944 tgss2 22973 neiptoptop 23118 restin 23153 restntr 23169 cnprest2 23277 pnrmopn 23330 cnrmnrm 23348 cmpsublem 23386 cmpsub 23387 cmpcld 23389 hausmapdom 23487 isref 23496 locfindis 23517 txbasex 23553 dfac14lem 23604 xkopt 23642 xkopjcn 23643 qtopval2 23683 elqtop 23684 fbssfi 23824 ptcmplem2 24040 cnextfval 24049 tuslem 24254 tuslemOLD 24255 madeval 27868 pliguhgr 30411 acunirnmpt2 32568 acunirnmpt2f 32569 ist0cld 33604 hasheuni 33874 insiga 33926 sigagenval 33929 omsval 34083 omssubadd 34090 sibfof 34130 sitmcl 34141 kur14 34996 cvmscld 35053 fobigcup 35672 hfuni 35956 isfne 35999 isfne4b 36001 fnemeet1 36026 tailfval 36032 bj-restuni2 36753 pibt2 37072 imaexALTV 37976 kelac2 42663 cnfex 44564 unidmex 44588 pwpwuni 44595 salgenval 45879 intsaluni 45887 salgenn0 45889 caragenunidm 46066 afv2ex 46764 iscnrm3rlem3 48213 |
Copyright terms: Public domain | W3C validator |