| 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 4918 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴) | |
| 2 | 1 | eleq1d 2826 | . 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V)) |
| 3 | vuniex 7759 | . 2 ⊢ ∪ 𝑥 ∈ V | |
| 4 | 2, 3 | vtoclg 3554 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 Vcvv 3480 ∪ cuni 4907 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-uni 4908 |
| This theorem is referenced by: uniex 7761 uniexd 7762 abnexg 7776 uniexb 7784 pwexr 7785 ssonuni 7800 ssonprc 7807 dmexg 7923 rnexg 7924 undefval 8301 onovuni 8382 tz7.44lem1 8445 tz7.44-3 8448 disjen 9174 domss2 9176 fival 9452 fipwuni 9466 supexd 9493 cantnflem1 9729 dfac8clem 10072 onssnum 10080 dfac12lem1 10184 dfac12lem2 10185 fin1a2lem12 10451 hsmexlem1 10466 wrdexb 14563 restid 17478 prdsbas 17502 prdsplusg 17503 prdsmulr 17504 prdsvsca 17505 prdshom 17512 sscpwex 17859 pmtrfv 19470 istopon 22918 tgval 22962 eltg2 22965 tgss2 22994 neiptoptop 23139 restin 23174 restntr 23190 cnprest2 23298 pnrmopn 23351 cnrmnrm 23369 cmpsublem 23407 cmpsub 23408 cmpcld 23410 hausmapdom 23508 isref 23517 locfindis 23538 txbasex 23574 dfac14lem 23625 xkopt 23663 xkopjcn 23664 qtopval2 23704 elqtop 23705 fbssfi 23845 ptcmplem2 24061 cnextfval 24070 tuslem 24275 tuslemOLD 24276 madeval 27891 pliguhgr 30505 acunirnmpt2 32670 acunirnmpt2f 32671 ist0cld 33832 hasheuni 34086 insiga 34138 sigagenval 34141 omsval 34295 omssubadd 34302 sibfof 34342 sitmcl 34353 kur14 35221 cvmscld 35278 fobigcup 35901 hfuni 36185 isfne 36340 isfne4b 36342 fnemeet1 36367 tailfval 36373 bj-restuni2 37099 pibt2 37418 imaexALTV 38331 kelac2 43077 cnfex 45033 unidmex 45055 pwpwuni 45062 salgenval 46336 intsaluni 46344 salgenn0 46346 caragenunidm 46523 afv2ex 47226 iscnrm3rlem3 48839 |
| Copyright terms: Public domain | W3C validator |