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 4536 | . 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵) | |
2 | ssexg 5230 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
3 | elpwg 4530 | . . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
4 | 3 | biimparc 483 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵) |
5 | 2, 4 | syldan 594 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵) |
6 | 5 | expcom 417 | . 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵)) |
7 | 1, 6 | impbid2 229 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∈ wcel 2111 Vcvv 3420 ⊆ wss 3880 𝒫 cpw 4527 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-ext 2709 ax-sep 5206 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-rab 3071 df-v 3422 df-in 3887 df-ss 3897 df-pw 4529 |
This theorem is referenced by: elpw2 5252 elpwi2OLD 5254 pwnss 5255 difelpw 5257 rabelpw 5258 pw2f1olem 8771 fineqvlem 8916 elfir 9055 r1sscl 9425 tskwe 9590 dfac8alem 9667 acni2 9684 fin1ai 9931 fin2i 9933 fin23lem7 9954 fin23lem11 9955 isfin2-2 9957 fin23lem39 9988 isf34lem1 10010 isf34lem2 10011 isf34lem4 10015 isf34lem5 10016 fin1a2lem12 10049 canthnumlem 10286 tsken 10392 tskss 10396 gruss 10434 ismre 17117 mreintcl 17122 mremre 17131 submre 17132 mrcval 17137 mrccl 17138 mrcun 17149 ismri 17158 acsfiel 17181 isacs1i 17184 catcoppccl 17647 catcoppcclOLD 17648 acsdrsel 18073 acsdrscl 18076 acsficl 18077 pmtrval 18867 pmtrrn 18873 istopg 21816 uniopn 21818 iscld 21948 ntrval 21957 clsval 21958 discld 22010 mretopd 22013 neival 22023 isnei 22024 lpval 22060 restdis 22099 ordtbaslem 22109 ordtuni 22111 cndis 22212 tgcmp 22322 hauscmplem 22327 comppfsc 22453 elkgen 22457 xkoopn 22510 elqtop 22618 kqffn 22646 isfbas 22750 filss 22774 snfbas 22787 elfg 22792 ufilss 22826 fixufil 22843 cfinufil 22849 ufinffr 22850 ufilen 22851 fin1aufil 22853 flimclslem 22905 hauspwpwf1 22908 supnfcls 22941 flimfnfcls 22949 ptcmplem1 22973 tsmsfbas 23049 blfvalps 23305 blfps 23328 blf 23329 bcthlem5 24249 minveclem3b 24349 sigaclcuni 31822 sigaclcu2 31824 pwsiga 31834 erdsze2lem2 32902 cvmsval 32964 cvmsss2 32972 neibastop2lem 34312 tailf 34327 pibt2 35351 fin2so 35527 sdclem1 35664 elrfirn 40248 elrfirn2 40249 istopclsd 40253 nacsfix 40265 dnnumch1 40600 inpw 45865 |
Copyright terms: Public domain | W3C validator |