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 4838 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴) | |
2 | 1 | eleq1d 2894 | . 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V)) |
3 | vuniex 7455 | . 2 ⊢ ∪ 𝑥 ∈ V | |
4 | 2, 3 | vtoclg 3565 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 Vcvv 3492 ∪ cuni 4830 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rex 3141 df-v 3494 df-uni 4831 |
This theorem is referenced by: uniexd 7457 abnexg 7467 uniexb 7475 pwexr 7476 ssonuni 7490 ssonprc 7496 dmexg 7602 rnexg 7603 undefval 7931 onovuni 7968 tz7.44lem1 8030 tz7.44-3 8033 en1uniel 8569 disjen 8662 domss2 8664 fival 8864 fipwuni 8878 supexd 8905 cantnflem1 9140 dfac8clem 9446 onssnum 9454 dfac12lem1 9557 dfac12lem2 9558 fin1a2lem12 9821 hsmexlem1 9836 wrdexb 13861 restid 16695 prdsbas 16718 prdsplusg 16719 prdsmulr 16720 prdsvsca 16721 prdshom 16728 sscpwex 17073 pmtrfv 18509 istopon 21448 tgval 21491 eltg2 21494 tgss2 21523 neiptoptop 21667 restin 21702 restntr 21718 cnprest2 21826 pnrmopn 21879 cnrmnrm 21897 cmpsublem 21935 cmpsub 21936 cmpcld 21938 hausmapdom 22036 isref 22045 locfindis 22066 txbasex 22102 dfac14lem 22153 xkopt 22191 xkopjcn 22192 qtopval2 22232 elqtop 22233 fbssfi 22373 ptcmplem2 22589 cnextfval 22598 tuslem 22803 pliguhgr 28190 elpwunicl 30234 acunirnmpt2 30333 acunirnmpt2f 30334 hasheuni 31243 insiga 31295 sigagenval 31298 omsval 31450 omssubadd 31457 sibfof 31497 sitmcl 31508 kur14 32360 cvmscld 32417 madeval 33186 fobigcup 33258 hfuni 33542 isfne 33584 isfne4b 33586 fnemeet1 33611 tailfval 33617 bj-restuni2 34283 pibt2 34580 imaexALTV 35468 kelac2 39543 cnfex 41162 unidmex 41189 pwpwuni 41196 salgenval 42483 intsaluni 42489 salgenn0 42491 caragenunidm 42667 afv2ex 43290 |
Copyright terms: Public domain | W3C validator |