Theorem snelpwi 5399

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 5398	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵))
2	1	ibi 267	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114  𝒫 cpw 4556  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-pw 4558  df-sn 4583  df-pr 4585

This theorem is referenced by:  unipw  5405  canth2  9070  pwfir  9229  unifpw  9267  marypha1lem  9348  infpwfidom  9950  ackbij1lem4  10144  acsfn  17594  sylow2a  19560  dissnref  23484  dissnlocfin  23485  locfindis  23486  txdis  23588  txdis1cn  23591  symgtgp  24062  1no  27818  bday0  27819  bday0b  27821  bday1  27822  cutneg  27824  cutlt  27940  oncutlt  28272  n0bday  28360  n0fincut  28363  bdayn0p1  28377  zcuts  28415  twocut  28431  addhalfcut  28467  dispcmp  34037  esumcst  34241  cntnevol  34406  coinflippvt  34663  onsucsuccmpi  36659  topdifinffinlem  37602  pclfinN  40276  lpirlnr  43474  unipwrVD  45187  unipwr  45188  salexct  46692  salexct3  46700  salgencntex  46701  salgensscntex  46702  sge0tsms  46738  sge0cl  46739  sge0sup  46749  isgrtri  48303  lincvalsng  48776  snlindsntor  48831