Theorem snelpwi 5443

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

Syntax hints:   → wi 4   ∈ wcel 2105  𝒫 cpw 4602  {csn 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3953  df-in 3955  df-ss 3965  df-pw 4604  df-sn 4629  df-pr 4631

This theorem is referenced by:  unipw  5450  canth2  9136  pwfir  9182  unifpw  9361  marypha1lem  9434  infpwfidom  10029  ackbij1lem4  10224  acsfn  17610  sylow2a  19535  dissnref  23351  dissnlocfin  23352  locfindis  23353  txdis  23455  txdis1cn  23458  symgtgp  23929  1sno  27672  bday0s  27673  bday0b  27675  bday1s  27676  cutlt  27764  dispcmp  33302  esumcst  33524  cntnevol  33689  coinflippvt  33946  onsucsuccmpi  35791  topdifinffinlem  36691  pclfinN  39234  lpirlnr  42321  unipwrVD  44055  unipwr  44056  salexct  45508  salexct3  45516  salgencntex  45517  salgensscntex  45518  sge0tsms  45554  sge0cl  45555  sge0sup  45565  lincvalsng  47258  snlindsntor  47313