| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elpwd | Structured version Visualization version GIF version | ||
| Description: Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| Ref | Expression |
|---|---|
| elpwd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| elpwd.2 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| Ref | Expression |
|---|---|
| elpwd | ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elpwd.2 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
| 2 | elpwd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
| 3 | elpwg 4603 | . . 3 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
| 4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
| 5 | 1, 4 | mpbird 257 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∈ wcel 2108 ⊆ 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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: sselpwd 5328 pwel 5381 frd 5641 f1opw2 7688 pwuncl 7790 naddunif 8731 f1opwfi 9396 ackbij1lem6 10264 ackbij1lem11 10269 mreacs 17701 sylow3lem3 19647 sylow3lem6 19650 cmpcov 23397 tgqtop 23720 filss 23861 scutval 27845 madecut 27921 cofcut1 27954 cutlt 27966 elons2d 28282 fnpreimac 32681 indval 32838 exsslsb 33647 pcmplfin 33859 rspectopn 33866 zarclsint 33871 zarcmplem 33880 reprval 34625 bj-sselpwuni 37051 bj-discrmoore 37112 dmvolss 46000 sge0xaddlem1 46448 meadjuni 46472 ovnval2b 46567 ovnsubadd2lem 46660 vonvolmbllem 46675 vonvolmbl 46676 smfresal 46803 smfpimbor1lem1 46813 sprsymrelfvlem 47477 isubgruhgr 47854 grimuhgr 47878 gpgedgel 48007 lindslinindsimp1 48374 lindslinindimp2lem4 48378 lincresunit3 48398 iscnrm3llem1 48846 |
| Copyright terms: Public domain | W3C validator |