![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elpw2g | Structured version Visualization version GIF version |
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |
Ref | Expression |
---|---|
elpw2g | ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpwi 4457 | . 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵) | |
2 | ssexg 5111 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
3 | elpwg 4455 | . . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
4 | 3 | biimparc 480 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵) |
5 | 2, 4 | syldan 591 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵) |
6 | 5 | expcom 414 | . 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵)) |
7 | 1, 6 | impbid2 227 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∈ wcel 2079 Vcvv 3432 ⊆ wss 3854 𝒫 cpw 4447 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-ext 2767 ax-sep 5088 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-v 3434 df-in 3861 df-ss 3869 df-pw 4449 |
This theorem is referenced by: elpw2 5132 elpwi2 5133 pwnss 5134 difelpw 5136 rabelpw 5137 pw2f1olem 8458 fineqvlem 8568 elfir 8715 r1sscl 9049 tskwe 9214 dfac8alem 9290 acni2 9307 fin1ai 9550 fin2i 9552 fin23lem7 9573 fin23lem11 9574 isfin2-2 9576 fin23lem39 9607 isf34lem1 9629 isf34lem2 9630 isf34lem4 9634 isf34lem5 9635 fin1a2lem12 9668 canthnumlem 9905 tsken 10011 tskss 10015 gruss 10053 ismre 16678 mreintcl 16683 mremre 16692 submre 16693 mrcval 16698 mrccl 16699 mrcun 16710 ismri 16719 acsfiel 16742 isacs1i 16745 catcoppccl 17185 acsdrsel 17594 acsdrscl 17597 acsficl 17598 pmtrval 18298 pmtrrn 18304 istopg 21175 uniopn 21177 iscld 21307 ntrval 21316 clsval 21317 discld 21369 mretopd 21372 neival 21382 isnei 21383 lpval 21419 restdis 21458 ordtbaslem 21468 ordtuni 21470 cndis 21571 tgcmp 21681 hauscmplem 21686 comppfsc 21812 elkgen 21816 xkoopn 21869 elqtop 21977 kqffn 22005 isfbas 22109 filss 22133 snfbas 22146 elfg 22151 ufilss 22185 fixufil 22202 cfinufil 22208 ufinffr 22209 ufilen 22210 fin1aufil 22212 flimclslem 22264 hauspwpwf1 22267 supnfcls 22300 flimfnfcls 22308 ptcmplem1 22332 tsmsfbas 22407 blfvalps 22664 blfps 22687 blf 22688 bcthlem5 23602 minveclem3b 23702 sigaclcuni 30950 sigaclcu2 30952 pwsiga 30962 erdsze2lem2 32015 cvmsval 32077 cvmsss2 32085 neibastop2lem 33262 tailf 33277 bj-ismoored 33945 pibt2 34175 fin2so 34356 sdclem1 34496 elrfirn 38727 elrfirn2 38728 istopclsd 38732 nacsfix 38744 dnnumch1 39080 |
Copyright terms: Public domain | W3C validator |