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 4168 | . 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵) | |
2 | ssexg 4804 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
3 | elpwg 4166 | . . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
4 | 3 | biimparc 504 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵) |
5 | 2, 4 | syldan 487 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵) |
6 | 5 | expcom 451 | . 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵)) |
7 | 1, 6 | impbid2 216 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∈ wcel 1990 Vcvv 3200 ⊆ wss 3574 𝒫 cpw 4158 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 df-ss 3588 df-pw 4160 |
This theorem is referenced by: elpw2 4828 elpwi2 4829 pwnss 4830 pw2f1olem 8064 fineqvlem 8174 elfir 8321 marypha1 8340 r1sscl 8648 tskwe 8776 dfac8alem 8852 acni2 8869 fin1ai 9115 fin2i 9117 fin23lem7 9138 fin23lem11 9139 isfin2-2 9141 fin23lem39 9172 isf34lem1 9194 isf34lem2 9195 isf34lem4 9199 isf34lem5 9200 fin1a2lem12 9233 canthnumlem 9470 canthp1lem2 9475 tsken 9576 tskss 9580 gruss 9618 ramub1lem1 15730 ismre 16250 mreintcl 16255 mremre 16264 submre 16265 mrcval 16270 mrccl 16271 mrcun 16282 ismri 16291 mreexexlem4d 16307 acsfiel 16315 isacs1i 16318 catcoppccl 16758 acsdrsel 17167 acsdrscl 17170 acsficl 17171 pmtrval 17871 pmtrrn 17877 opsrval 19474 istopg 20700 uniopn 20702 iscld 20831 ntrval 20840 clsval 20841 discld 20893 mretopd 20896 neival 20906 isnei 20907 lpval 20943 restdis 20982 ordtbaslem 20992 ordtuni 20994 cncls 21078 cndis 21095 tgcmp 21204 hauscmplem 21209 comppfsc 21335 elkgen 21339 xkoopn 21392 elqtop 21500 kqffn 21528 isfbas 21633 filss 21657 snfbas 21670 elfg 21675 fbasrn 21688 ufilss 21709 fixufil 21726 cfinufil 21732 ufinffr 21733 ufilen 21734 fin1aufil 21736 rnelfmlem 21756 flimclslem 21788 hauspwpwf1 21791 supnfcls 21824 flimfnfcls 21832 ptcmplem1 21856 tsmsfbas 21931 blfvalps 22188 blfps 22211 blf 22212 bcthlem5 23125 minveclem3b 23199 sigaclcuni 30181 sigaclcu2 30183 pwsiga 30193 erdsze2lem2 31186 cvmsval 31248 cvmsss2 31256 neibastop2lem 32355 tailf 32370 bj-ismoored 33062 fin2so 33396 sdclem1 33539 elrfirn 37258 elrfirn2 37259 istopclsd 37263 nacsfix 37275 dnnumch1 37614 |
Copyright terms: Public domain | W3C validator |