![]() |
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 4571 | . 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵) | |
2 | ssexg 5284 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
3 | elpwg 4567 | . . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
4 | 3 | biimparc 481 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵) |
5 | 2, 4 | syldan 592 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵) |
6 | 5 | expcom 415 | . 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵)) |
7 | 1, 6 | impbid2 225 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2107 Vcvv 3447 ⊆ wss 3914 𝒫 cpw 4564 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5260 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-v 3449 df-in 3921 df-ss 3931 df-pw 4566 |
This theorem is referenced by: elpw2 5306 elpwi2OLD 5308 pwnss 5310 difelpw 5312 rabelpw 5313 pw2f1olem 9026 fineqvlem 9212 elfir 9359 r1sscl 9729 tskwe 9894 dfac8alem 9973 acni2 9990 fin1ai 10237 fin2i 10239 fin23lem7 10260 fin23lem11 10261 isfin2-2 10263 fin23lem39 10294 isf34lem1 10316 isf34lem2 10317 isf34lem4 10321 isf34lem5 10322 fin1a2lem12 10355 canthnumlem 10592 tsken 10698 tskss 10702 gruss 10740 ismre 17478 mreintcl 17483 mremre 17492 submre 17493 mrcval 17498 mrccl 17499 mrcun 17510 ismri 17519 acsfiel 17542 isacs1i 17545 catcoppccl 18011 catcoppcclOLD 18012 acsdrsel 18440 acsdrscl 18443 acsficl 18444 pmtrval 19241 pmtrrn 19247 istopg 22267 uniopn 22269 iscld 22401 ntrval 22410 clsval 22411 discld 22463 mretopd 22466 neival 22476 isnei 22477 lpval 22513 restdis 22552 ordtbaslem 22562 ordtuni 22564 cndis 22665 tgcmp 22775 hauscmplem 22780 comppfsc 22906 elkgen 22910 xkoopn 22963 elqtop 23071 kqffn 23099 isfbas 23203 filss 23227 snfbas 23240 elfg 23245 ufilss 23279 fixufil 23296 cfinufil 23302 ufinffr 23303 ufilen 23304 fin1aufil 23306 flimclslem 23358 hauspwpwf1 23361 supnfcls 23394 flimfnfcls 23402 ptcmplem1 23426 tsmsfbas 23502 blfvalps 23759 blfps 23782 blf 23783 bcthlem5 24715 minveclem3b 24815 sigaclcuni 32781 sigaclcu2 32783 pwsiga 32793 erdsze2lem2 33862 cvmsval 33924 cvmsss2 33932 neibastop2lem 34885 tailf 34900 pibt2 35938 fin2so 36115 sdclem1 36252 elrfirn 41065 elrfirn2 41066 istopclsd 41070 nacsfix 41082 dnnumch1 41418 inpw 46993 |
Copyright terms: Public domain | W3C validator |