![]() |
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 3427), 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 4721 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴) | |
3 | 2 | eleq1d 2850 | . 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V)) |
4 | uniex2 7284 | . . 3 ⊢ ∃𝑦 𝑦 = ∪ 𝑥 | |
5 | 4 | issetri 3431 | . 2 ⊢ ∪ 𝑥 ∈ V |
6 | 1, 3, 5 | vtocl 3478 | 1 ⊢ ∪ 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 ∈ wcel 2050 Vcvv 3415 ∪ cuni 4713 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-sep 5061 ax-un 7281 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-rex 3094 df-v 3417 df-uni 4714 |
This theorem is referenced by: vuniex 7286 unex 7288 iunpw 7311 elxp4 7444 elxp5 7445 1stval 7505 2ndval 7506 fo1st 7523 fo2nd 7524 cnvf1o 7616 brtpos2 7703 ixpsnf1o 8301 dffi3 8692 cnfcom2 8961 cnfcom3lem 8962 cnfcom3 8963 trcl 8966 rankc2 9096 rankxpl 9100 rankxpsuc 9107 acnlem 9270 dfac2a 9351 fin23lem14 9555 fin23lem16 9557 fin23lem17 9560 fin23lem38 9571 fin23lem39 9572 itunisuc 9641 axdc3lem2 9673 axcclem 9679 ac5b 9700 ttukey 9740 wunex2 9960 wuncval2 9969 intgru 10036 pnfex 10495 prdsval 16587 prdsds 16596 wunfunc 17030 wunnat 17087 arwval 17164 catcfuccl 17230 catcxpccl 17318 zrhval 20360 mreclatdemoBAD 21411 ptbasin2 21893 ptbasfi 21896 dfac14 21933 ptcmplem2 22368 ptcmplem3 22369 ptcmp 22373 cnextfvval 22380 cnextcn 22382 minveclem4a 23739 xrge0tsmsbi 30531 dimval 30630 dimvalfi 30631 locfinreflem 30748 pstmfval 30780 pstmxmet 30781 esumex 30932 msrval 32305 dfrdg2 32561 trpredex 32597 fvbigcup 32884 ctbssinf 34128 ptrest 34332 heiborlem1 34531 heiborlem3 34533 heibor 34541 dicval 37757 aomclem1 39050 dfac21 39062 ntrrn 39835 ntrf 39836 dssmapntrcls 39841 fourierdlem70 41893 caragendifcl 42228 cnfsmf 42449 setrec1lem3 44160 setrec2fun 44163 |
Copyright terms: Public domain | W3C validator |