Theorem snelpwi 5442

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

Syntax hints:   → wi 4   ∈ wcel 2104  𝒫 cpw 4601  {csn 4627

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952  df-in 3954  df-ss 3964  df-pw 4603  df-sn 4628  df-pr 4630

This theorem is referenced by:  unipw  5449  canth2  9132  pwfir  9178  unifpw  9357  marypha1lem  9430  infpwfidom  10025  ackbij1lem4  10220  acsfn  17607  sylow2a  19528  dissnref  23252  dissnlocfin  23253  locfindis  23254  txdis  23356  txdis1cn  23359  symgtgp  23830  1sno  27565  bday0s  27566  bday0b  27568  bday1s  27569  cutlt  27657  dispcmp  33137  esumcst  33359  cntnevol  33524  coinflippvt  33781  onsucsuccmpi  35631  topdifinffinlem  36531  pclfinN  39074  lpirlnr  42161  unipwrVD  43895  unipwr  43896  salexct  45348  salexct3  45356  salgencntex  45357  salgensscntex  45358  sge0tsms  45394  sge0cl  45395  sge0sup  45405  lincvalsng  47184  snlindsntor  47239