![]() |
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 4561 | . . 3 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
5 | 1, 4 | mpbird 256 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2106 ⊆ wss 3908 𝒫 cpw 4558 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3445 df-in 3915 df-ss 3925 df-pw 4560 |
This theorem is referenced by: sselpwd 5281 pwel 5334 frd 5590 f1opw2 7600 pwuncl 7696 f1opwfi 9258 ackbij1lem6 10119 ackbij1lem11 10124 mreacs 17497 sylow3lem3 19369 sylow3lem6 19372 cmpcov 22691 tgqtop 23014 filss 23155 scutval 27090 madecut 27162 cofcut1 27187 fnpreimac 31414 pcmplfin 32244 rspectopn 32251 zarclsint 32256 zarcmplem 32265 indval 32415 reprval 33026 naddunif 34240 bj-sselpwuni 35452 bj-discrmoore 35513 dmvolss 44120 sge0xaddlem1 44568 meadjuni 44592 ovnval2b 44687 ovnsubadd2lem 44780 vonvolmbllem 44795 vonvolmbl 44796 smfresal 44923 smfpimbor1lem1 44933 sprsymrelfvlem 45576 lindslinindsimp1 46432 lindslinindimp2lem4 46436 lincresunit3 46456 iscnrm3llem1 46876 |
Copyright terms: Public domain | W3C validator |