Theorem snelpwi 5396

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

Syntax hints:   → wi 4   ∈ wcel 2114  𝒫 cpw 4541  {csn 4567

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-pw 4543  df-sn 4568  df-pr 4570

This theorem is referenced by:  unipw  5402  canth2  9068  pwfir  9227  unifpw  9265  marypha1lem  9346  infpwfidom  9950  ackbij1lem4  10144  acsfn  17625  sylow2a  19594  dissnref  23493  dissnlocfin  23494  locfindis  23495  txdis  23597  txdis1cn  23600  symgtgp  24071  1no  27802  bday0  27803  bday0b  27805  bday1  27806  cutneg  27808  cutlt  27924  oncutlt  28256  n0bday  28344  n0fincut  28347  bdayn0p1  28361  zcuts  28399  twocut  28415  addhalfcut  28451  dispcmp  34003  esumcst  34207  cntnevol  34372  coinflippvt  34629  onsucsuccmpi  36625  topdifinffinlem  37663  pclfinN  40346  lpirlnr  43545  unipwrVD  45258  unipwr  45259  salexct  46762  salexct3  46770  salgencntex  46771  salgensscntex  46772  sge0tsms  46808  sge0cl  46809  sge0sup  46819  isgrtri  48419  lincvalsng  48892  snlindsntor  48947