| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > snelpwi | Structured version Visualization version GIF version | ||
| Description: If a set is a member of a class, then the singleton of that set is a member of the powerclass of that class. (Contributed by Alan Sare, 25-Aug-2011.) |
| Ref | Expression |
|---|---|
| snelpwi | ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | snelpwg 5447 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵)) | |
| 2 | 1 | ibi 267 | 1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 𝒫 cpw 4600 {csn 4626 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-ss 3968 df-pw 4602 df-sn 4627 df-pr 4629 |
| This theorem is referenced by: unipw 5455 canth2 9170 pwfir 9355 unifpw 9395 marypha1lem 9473 infpwfidom 10068 ackbij1lem4 10262 acsfn 17702 sylow2a 19637 dissnref 23536 dissnlocfin 23537 locfindis 23538 txdis 23640 txdis1cn 23643 symgtgp 24114 1sno 27872 bday0s 27873 bday0b 27875 bday1s 27876 cutlt 27966 n0sbday 28354 zscut 28393 1p1e2s 28400 nohalf 28407 addhalfcut 28419 dispcmp 33858 esumcst 34064 cntnevol 34229 coinflippvt 34487 onsucsuccmpi 36444 topdifinffinlem 37348 pclfinN 39902 lpirlnr 43129 unipwrVD 44852 unipwr 44853 salexct 46349 salexct3 46357 salgencntex 46358 salgensscntex 46359 sge0tsms 46395 sge0cl 46396 sge0sup 46406 isgrtri 47910 lincvalsng 48333 snlindsntor 48388 |
| Copyright terms: Public domain | W3C validator |