![]() |
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 7220 | . 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V) | |
2 | uniexr 7237 | . 2 ⊢ (∪ 𝐴 ∈ V → 𝐴 ∈ V) | |
3 | 1, 2 | impbii 201 | 1 ⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∈ wcel 2164 Vcvv 3414 ∪ cuni 4660 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-8 2166 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 ax-sep 5007 ax-pow 5067 ax-un 7214 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rex 3123 df-v 3416 df-in 3805 df-ss 3812 df-pw 4382 df-uni 4661 |
This theorem is referenced by: elpwpwel 7241 ixpexg 8205 rankuni 9010 unialeph 9244 ttukeylem1 9653 tgss2 21169 ordtbas2 21373 ordtbas 21374 ordttopon 21375 ordtopn1 21376 ordtopn2 21377 ordtrest2 21386 isref 21690 islocfin 21698 txbasex 21747 ptbasin2 21759 ordthmeolem 21982 alexsublem 22225 alexsub 22226 alexsubb 22227 ussid 22441 ordtrest2NEW 30510 omsfval 30897 brbigcup 32539 isfne 32867 isfne4 32868 isfne4b 32869 fnessref 32885 neibastop1 32887 fnejoin2 32897 prtex 34950 |
Copyright terms: Public domain | W3C validator |