![]() |
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 4607 | . 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵) | |
2 | ssexg 5321 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
3 | elpwg 4603 | . . . . 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 3475 ⊆ wss 3946 𝒫 cpw 4600 |
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 5297 |
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 3434 df-v 3477 df-in 3953 df-ss 3963 df-pw 4602 |
This theorem is referenced by: elpw2 5343 elpwi2OLD 5345 pwnss 5347 difelpw 5349 rabelpw 5350 pw2f1olem 9071 fineqvlem 9257 elfir 9405 r1sscl 9775 tskwe 9940 dfac8alem 10019 acni2 10036 fin1ai 10283 fin2i 10285 fin23lem7 10306 fin23lem11 10307 isfin2-2 10309 fin23lem39 10340 isf34lem1 10362 isf34lem2 10363 isf34lem4 10367 isf34lem5 10368 fin1a2lem12 10401 canthnumlem 10638 tsken 10744 tskss 10748 gruss 10786 ismre 17529 mreintcl 17534 mremre 17543 submre 17544 mrcval 17549 mrccl 17550 mrcun 17561 ismri 17570 acsfiel 17593 isacs1i 17596 catcoppccl 18062 catcoppcclOLD 18063 acsdrsel 18491 acsdrscl 18494 acsficl 18495 pmtrval 19311 pmtrrn 19317 istopg 22378 uniopn 22380 iscld 22512 ntrval 22521 clsval 22522 discld 22574 mretopd 22577 neival 22587 isnei 22588 lpval 22624 restdis 22663 ordtbaslem 22673 ordtuni 22675 cndis 22776 tgcmp 22886 hauscmplem 22891 comppfsc 23017 elkgen 23021 xkoopn 23074 elqtop 23182 kqffn 23210 isfbas 23314 filss 23338 snfbas 23351 elfg 23356 ufilss 23390 fixufil 23407 cfinufil 23413 ufinffr 23414 ufilen 23415 fin1aufil 23417 flimclslem 23469 hauspwpwf1 23472 supnfcls 23505 flimfnfcls 23513 ptcmplem1 23537 tsmsfbas 23613 blfvalps 23870 blfps 23893 blf 23894 bcthlem5 24826 minveclem3b 24926 sigaclcuni 33053 sigaclcu2 33055 pwsiga 33065 erdsze2lem2 34132 cvmsval 34194 cvmsss2 34202 neibastop2lem 35182 tailf 35197 pibt2 36235 fin2so 36412 sdclem1 36548 elrfirn 41365 elrfirn2 41366 istopclsd 41370 nacsfix 41382 dnnumch1 41718 inpw 47404 |
Copyright terms: Public domain | W3C validator |