![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uniexb | Structured version Visualization version GIF version |
Description: The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003.) |
Ref | Expression |
---|---|
uniexb | ⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniexg 7746 | . 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V) | |
2 | uniexr 7766 | . 2 ⊢ (∪ 𝐴 ∈ V → 𝐴 ∈ V) | |
3 | 1, 2 | impbii 208 | 1 ⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∈ wcel 2098 Vcvv 3461 ∪ cuni 4909 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-pow 5365 ax-un 7741 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1086 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-in 3951 df-ss 3961 df-pw 4606 df-uni 4910 |
This theorem is referenced by: elpwpwel 7770 ixpexg 8941 rankuni 9888 unialeph 10126 ttukeylem1 10534 tgss2 22934 ordtbas2 23139 ordtbas 23140 ordttopon 23141 ordtopn1 23142 ordtopn2 23143 ordtrest2 23152 isref 23457 islocfin 23465 txbasex 23514 ptbasin2 23526 ordthmeolem 23749 alexsublem 23992 alexsub 23993 alexsubb 23994 ussid 24209 ordtrest2NEW 33652 brbigcup 35622 isfne 35951 isfne4 35952 isfne4b 35953 fnessref 35969 neibastop1 35971 fnejoin2 35981 prtex 38479 |
Copyright terms: Public domain | W3C validator |