![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pwidg | Structured version Visualization version GIF version |
Description: A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Ref | Expression |
---|---|
pwidg | ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 4002 | . 2 ⊢ 𝐴 ⊆ 𝐴 | |
2 | elpwg 4601 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐴 ↔ 𝐴 ⊆ 𝐴)) | |
3 | 1, 2 | mpbiri 258 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ⊆ wss 3946 𝒫 cpw 4598 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3953 df-ss 3963 df-pw 4600 |
This theorem is referenced by: pwidb 4619 pwid 4620 axpweq 5344 knatar 7341 brwdom2 9555 pwwf 9789 rankpwi 9805 canthp1lem2 10635 canthp1 10636 mremre 17535 submre 17536 baspartn 22426 fctop 22476 cctop 22478 ppttop 22479 epttop 22481 isopn3 22539 mretopd 22565 tsmsfbas 23601 gsumesum 32988 esumcst 32992 pwsiga 33059 prsiga 33060 sigainb 33065 pwldsys 33086 ldgenpisyslem1 33092 carsggect 33248 ex-sategoelel 34343 neibastop1 35149 neibastop2lem 35150 topdifinfindis 36132 elrfi 41303 dssmapnvod 42642 ntrk0kbimka 42661 clsk3nimkb 42662 neik0pk1imk0 42669 ntrclscls00 42688 ntrneicls00 42711 pwssfi 43603 dvnprodlem3 44537 caragenunidm 45097 |
Copyright terms: Public domain | W3C validator |