Theorem snelpwi 5444

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.)

Assertion

Ref	Expression
snelpwi	⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Proof of Theorem snelpwi

Step	Hyp	Ref	Expression
1		snelpwg 5443	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵))
2	1	ibi 267	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2107  𝒫 cpw 4603  {csn 4629

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  ax-sep 5300  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-pw 4605  df-sn 4630  df-pr 4632

This theorem is referenced by:  unipw  5451  canth2  9130  pwfir  9176  unifpw  9355  marypha1lem  9428  infpwfidom  10023  ackbij1lem4  10218  acsfn  17603  sylow2a  19487  dissnref  23032  dissnlocfin  23033  locfindis  23034  txdis  23136  txdis1cn  23139  symgtgp  23610  1sno  27328  bday0s  27329  bday0b  27331  bday1s  27332  cutlt  27419  dispcmp  32839  esumcst  33061  cntnevol  33226  coinflippvt  33483  onsucsuccmpi  35328  topdifinffinlem  36228  pclfinN  38771  lpirlnr  41859  unipwrVD  43593  unipwr  43594  salexct  45050  salexct3  45058  salgencntex  45059  salgensscntex  45060  sge0tsms  45096  sge0cl  45097  sge0sup  45107  lincvalsng  47097  snlindsntor  47152