Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pwidg | Structured version Visualization version GIF version |
Description: Membership of the original in a power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Ref | Expression |
---|---|
pwidg | ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 3587 | . 2 ⊢ 𝐴 ⊆ 𝐴 | |
2 | elpwg 4116 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐴 ↔ 𝐴 ⊆ 𝐴)) | |
3 | 1, 2 | mpbiri 247 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 ⊆ wss 3540 𝒫 cpw 4108 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 df-ss 3554 df-pw 4110 |
This theorem is referenced by: pwid 4122 axpweq 4768 knatar 6507 brwdom2 8361 pwwf 8553 rankpwi 8569 canthp1lem2 9354 canthp1 9355 grothpw 9527 mremre 16087 submre 16088 baspartn 20569 fctop 20618 cctop 20620 ppttop 20621 epttop 20623 isopn3 20680 mretopd 20706 tsmsfbas 21741 gsumesum 29448 esumcst 29452 pwsiga 29520 prsiga 29521 sigainb 29526 pwldsys 29547 ldgenpisyslem1 29553 carsggect 29707 neibastop1 31524 neibastop2lem 31525 topdifinfindis 32370 elrfi 36275 dssmapnvod 37334 ntrk0kbimka 37357 clsk3nimkb 37358 neik0pk1imk0 37365 ntrclscls00 37384 ntrneicls00 37407 pwssfi 38236 dvnprodlem3 38838 caragenunidm 39398 |
Copyright terms: Public domain | W3C validator |