Theorem snelpwi 5386

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

Syntax hints:   → wi 4   ∈ wcel 2109  𝒫 cpw 4551  {csn 4577

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920  df-pw 4553  df-sn 4578  df-pr 4580

This theorem is referenced by:  unipw  5393  canth2  9047  pwfir  9206  unifpw  9245  marypha1lem  9323  infpwfidom  9922  ackbij1lem4  10116  acsfn  17565  sylow2a  19498  dissnref  23413  dissnlocfin  23414  locfindis  23415  txdis  23517  txdis1cn  23520  symgtgp  23991  1sno  27741  bday0s  27742  bday0b  27744  bday1s  27745  cutneg  27747  cutlt  27845  onscutlt  28170  n0sbday  28249  n0sfincut  28251  bdayn0p1  28263  zscut  28300  1p1e2s  28308  twocut  28315  addhalfcut  28347  dispcmp  33826  esumcst  34030  cntnevol  34195  coinflippvt  34453  onsucsuccmpi  36421  topdifinffinlem  37325  pclfinN  39883  lpirlnr  43094  unipwrVD  44809  unipwr  44810  salexct  46319  salexct3  46327  salgencntex  46328  salgensscntex  46329  sge0tsms  46365  sge0cl  46366  sge0sup  46376  isgrtri  47931  lincvalsng  48405  snlindsntor  48460