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 3507), 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 4840 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴) | |
3 | 2 | eleq1d 2897 | . 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V)) |
4 | uniex2 7453 | . . 3 ⊢ ∃𝑦 𝑦 = ∪ 𝑥 | |
5 | 4 | issetri 3511 | . 2 ⊢ ∪ 𝑥 ∈ V |
6 | 1, 3, 5 | vtocl 3560 | 1 ⊢ ∪ 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∈ wcel 2105 Vcvv 3495 ∪ cuni 4832 |
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 2793 ax-sep 5195 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 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rex 3144 df-v 3497 df-uni 4833 |
This theorem is referenced by: vuniex 7455 unex 7457 iunpw 7481 elxp4 7615 elxp5 7616 1stval 7682 2ndval 7683 fo1st 7700 fo2nd 7701 cnvf1o 7797 brtpos2 7889 ixpsnf1o 8491 dffi3 8884 cnfcom2 9154 cnfcom3lem 9155 cnfcom3 9156 trcl 9159 rankc2 9289 rankxpl 9293 rankxpsuc 9300 acnlem 9463 dfac2a 9544 fin23lem14 9744 fin23lem16 9746 fin23lem17 9749 fin23lem38 9760 fin23lem39 9761 itunisuc 9830 axdc3lem2 9862 axcclem 9868 ac5b 9889 ttukey 9929 wunex2 10149 wuncval2 10158 intgru 10225 pnfex 10683 prdsval 16718 prdsds 16727 wunfunc 17159 wunnat 17216 arwval 17293 catcfuccl 17359 catcxpccl 17447 zrhval 20585 mreclatdemoBAD 21634 ptbasin2 22116 ptbasfi 22119 dfac14 22156 ptcmplem2 22591 ptcmplem3 22592 ptcmp 22596 cnextfvval 22603 cnextcn 22605 minveclem4a 23962 xrge0tsmsbi 30621 dimval 30901 dimvalfi 30902 locfinreflem 31004 pstmfval 31036 pstmxmet 31037 esumex 31188 msrval 32683 dfrdg2 32938 trpredex 32974 fvbigcup 33261 ctbssinf 34570 ptrest 34773 heiborlem1 34972 heiborlem3 34974 heibor 34982 dicval 38194 aomclem1 39534 dfac21 39546 ntrrn 40352 ntrf 40353 dssmapntrcls 40358 fourierdlem70 42342 caragendifcl 42677 cnfsmf 42898 setrec1lem3 44690 setrec2fun 44693 |
Copyright terms: Public domain | W3C validator |