Theorem snelpwi 5406

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

Syntax hints:   → wi 4   ∈ wcel 2109  𝒫 cpw 4566  {csn 4592

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 2702  ax-sep 5254  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-pw 4568  df-sn 4593  df-pr 4595

This theorem is referenced by:  unipw  5413  canth2  9100  pwfir  9273  unifpw  9313  marypha1lem  9391  infpwfidom  9988  ackbij1lem4  10182  acsfn  17627  sylow2a  19556  dissnref  23422  dissnlocfin  23423  locfindis  23424  txdis  23526  txdis1cn  23529  symgtgp  24000  1sno  27746  bday0s  27747  bday0b  27749  bday1s  27750  cutneg  27752  cutlt  27847  onscutlt  28172  n0sbday  28251  n0sfincut  28253  bdayn0p1  28265  zscut  28302  1p1e2s  28309  twocut  28316  addhalfcut  28341  dispcmp  33856  esumcst  34060  cntnevol  34225  coinflippvt  34483  onsucsuccmpi  36438  topdifinffinlem  37342  pclfinN  39901  lpirlnr  43113  unipwrVD  44828  unipwr  44829  salexct  46339  salexct3  46347  salgencntex  46348  salgensscntex  46349  sge0tsms  46385  sge0cl  46386  sge0sup  46396  isgrtri  47946  lincvalsng  48409  snlindsntor  48464