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 4516 | . . 3 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
5 | 1, 4 | mpbird 260 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∈ wcel 2110 ⊆ wss 3866 𝒫 cpw 4513 |
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 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-in 3873 df-ss 3883 df-pw 4515 |
This theorem is referenced by: sselpwd 5219 pwel 5274 f1opw2 7460 pwuncl 7555 f1opwfi 8980 ackbij1lem6 9839 ackbij1lem11 9844 mreacs 17161 sylow3lem3 19018 sylow3lem6 19021 cmpcov 22286 tgqtop 22609 filss 22750 fnpreimac 30728 pcmplfin 31524 rspectopn 31531 zarclsint 31536 zarcmplem 31545 indval 31693 reprval 32302 scutval 33731 madecut 33802 cofcut1 33827 bj-sselpwuni 34960 bj-discrmoore 35017 dmvolss 43201 sge0xaddlem1 43646 meadjuni 43670 ovnval2b 43765 ovnsubadd2lem 43858 vonvolmbllem 43873 vonvolmbl 43874 smfresal 43994 smfpimbor1lem1 44004 sprsymrelfvlem 44615 lindslinindsimp1 45471 lindslinindimp2lem4 45475 lincresunit3 45495 iscnrm3llem1 45916 |
Copyright terms: Public domain | W3C validator |