Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uniex | Structured version Visualization version GIF version |
Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3180), then the union of 𝐴 is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.) |
Ref | Expression |
---|---|
uniex.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
uniex | ⊢ ∪ 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | unieq 4380 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴) | |
3 | 2 | eleq1d 2672 | . 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V)) |
4 | uniex2 6850 | . . 3 ⊢ ∃𝑦 𝑦 = ∪ 𝑥 | |
5 | 4 | issetri 3183 | . 2 ⊢ ∪ 𝑥 ∈ V |
6 | 1, 3, 5 | vtocl 3232 | 1 ⊢ ∪ 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∈ wcel 1977 Vcvv 3173 ∪ cuni 4372 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-un 6847 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-v 3175 df-uni 4373 |
This theorem is referenced by: vuniex 6852 unex 6854 iunpw 6870 elxp4 7003 elxp5 7004 1stval 7061 2ndval 7062 fo1st 7079 fo2nd 7080 cnvf1o 7163 brtpos2 7245 ixpsnf1o 7834 dffi3 8220 cnfcom2 8482 cnfcom3lem 8483 cnfcom3 8484 trcl 8487 rankc2 8617 rankxpl 8621 rankxpsuc 8628 acnlem 8754 dfac2a 8835 fin23lem14 9038 fin23lem16 9040 fin23lem17 9043 fin23lem38 9054 fin23lem39 9055 itunisuc 9124 axdc3lem2 9156 axcclem 9162 ac5b 9183 ttukey 9223 wunex2 9439 wuncval2 9448 intgru 9515 pnfxr 9971 prdsval 15938 prdsds 15947 wunfunc 16382 wunnat 16439 arwval 16516 catcfuccl 16582 catcxpccl 16670 zrhval 19675 mreclatdemoBAD 20710 ptbasin2 21191 ptbasfi 21194 dfac14 21231 ptcmplem2 21667 ptcmplem3 21668 ptcmp 21672 cnextfvval 21679 cnextcn 21681 minveclem4a 23009 xrge0tsmsbi 29117 locfinreflem 29235 pstmfval 29267 pstmxmet 29268 esumex 29418 msrval 30689 dfrdg2 30945 trpredex 30981 fvbigcup 31179 ptrest 32578 heiborlem1 32780 heiborlem3 32782 heibor 32790 dicval 35483 aomclem1 36642 dfac21 36654 ntrrn 37440 ntrf 37441 dssmapntrcls 37446 fourierdlem70 39069 caragendifcl 39404 cnfsmf 39627 setrec1lem3 42235 setrec2fun 42238 |
Copyright terms: Public domain | W3C validator |