| 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 5323 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
| 3 | elpwg 4603 | . . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
| 4 | 3 | biimparc 479 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵) |
| 5 | 2, 4 | syldan 591 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵) |
| 6 | 5 | expcom 413 | . 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵)) |
| 7 | 1, 6 | impbid2 226 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∈ wcel 2108 Vcvv 3480 ⊆ wss 3951 𝒫 cpw 4600 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-in 3958 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: elpw2 5334 rabelpw 5336 difelpw 5354 pw2f1olem 9116 fineqvlem 9298 elfir 9455 r1sscl 9825 tskwe 9990 dfac8alem 10069 acni2 10086 fin1ai 10333 fin2i 10335 fin23lem7 10356 fin23lem11 10357 isfin2-2 10359 fin23lem39 10390 isf34lem1 10412 isf34lem2 10413 isf34lem4 10417 isf34lem5 10418 fin1a2lem12 10451 canthnumlem 10688 tsken 10794 tskss 10798 gruss 10836 ismre 17633 mreintcl 17638 mremre 17647 submre 17648 mrcval 17653 mrccl 17654 mrcun 17665 ismri 17674 acsfiel 17697 isacs1i 17700 catcoppccl 18162 acsdrsel 18588 acsdrscl 18591 acsficl 18592 pmtrval 19469 pmtrrn 19475 istopg 22901 uniopn 22903 iscld 23035 ntrval 23044 clsval 23045 discld 23097 mretopd 23100 neival 23110 isnei 23111 lpval 23147 restdis 23186 ordtbaslem 23196 ordtuni 23198 cndis 23299 tgcmp 23409 hauscmplem 23414 comppfsc 23540 elkgen 23544 xkoopn 23597 elqtop 23705 kqffn 23733 isfbas 23837 filss 23861 snfbas 23874 elfg 23879 ufilss 23913 fixufil 23930 cfinufil 23936 ufinffr 23937 ufilen 23938 fin1aufil 23940 flimclslem 23992 hauspwpwf1 23995 supnfcls 24028 flimfnfcls 24036 ptcmplem1 24060 tsmsfbas 24136 blfvalps 24393 blfps 24416 blf 24417 bcthlem5 25362 minveclem3b 25462 sigaclcuni 34119 sigaclcu2 34121 pwsiga 34131 erdsze2lem2 35209 cvmsval 35271 cvmsss2 35279 neibastop2lem 36361 tailf 36376 pibt2 37418 fin2so 37614 sdclem1 37750 elrfirn 42706 elrfirn2 42707 istopclsd 42711 nacsfix 42723 dnnumch1 43056 inpw 48738 |
| Copyright terms: Public domain | W3C validator |