Theorem snelpwi 5425

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

Syntax hints:   → wi 4   ∈ wcel 2143  𝒫 cpw 4562  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-pw 4564  df-sn 4590  df-pr 4592

This theorem is referenced by:  unipw  5431  canth2  9114  pwfir  9272  unifpw  9308  marypha1lem  9389  infpwfidom  10008  ackbij1lem4  10201  acsfn  17710  sylow2a  19684  dissnref  23685  dissnlocfin  23686  locfindis  23687  txdis  23789  txdis1cn  23792  symgtgp  24263  1no  28003  bday0  28004  bday0b  28006  bday1  28007  cutneg  28009  cutlt  28125  oncutlt  28457  n0bday  28545  n0fincut  28548  bdayn0p1  28562  zcuts  28600  twocut  28616  addhalfcut  28652  dispcmp  34249  esumcst  34453  cntnevol  34618  coinflippvt  34875  onsucsuccmpi  36954  topdifinffinlem  37993  pclfinN  40674  lpirlnr  43844  unipwrVD  45540  unipwr  45541  salexct  47048  salexct3  47056  salgencntex  47057  salgensscntex  47058  sge0tsms  47094  sge0cl  47095  sge0sup  47105  isgrtri  48708  lincvalsng  49196  snlindsntor  49251