Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > snelpwi | Structured version Visualization version GIF version |
Description: A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.) |
Ref | Expression |
---|---|
snelpwi | ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snssi 4736 | . 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) | |
2 | snex 5339 | . . 3 ⊢ {𝐴} ∈ V | |
3 | 2 | elpw 4532 | . 2 ⊢ ({𝐴} ∈ 𝒫 𝐵 ↔ {𝐴} ⊆ 𝐵) |
4 | 1, 3 | sylibr 237 | 1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2111 ⊆ wss 3881 𝒫 cpw 4528 {csn 4556 |
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 2113 ax-9 2121 ax-ext 2709 ax-sep 5207 ax-nul 5214 ax-pr 5337 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-v 3423 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4253 df-pw 4530 df-sn 4557 df-pr 4559 |
This theorem is referenced by: unipw 5350 canth2 8822 pwfir 8877 unifpw 9004 marypha1lem 9074 infpwfidom 9667 ackbij1lem4 9862 acsfn 17187 sylow2a 19033 dissnref 22449 dissnlocfin 22450 locfindis 22451 txdis 22553 txdis1cn 22556 symgtgp 23027 dispcmp 31547 esumcst 31767 cntnevol 31932 coinflippvt 32187 1sno 33784 bday0s 33785 bday0b 33787 bday1s 33788 onsucsuccmpi 34395 topdifinffinlem 35282 pclfinN 37678 lpirlnr 40674 unipwrVD 42154 unipwr 42155 salexct 43577 salexct3 43585 salgencntex 43586 salgensscntex 43587 sge0tsms 43622 sge0cl 43623 sge0sup 43633 lincvalsng 45459 snlindsntor 45514 |
Copyright terms: Public domain | W3C validator |