Theorem snelpwi 5411

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

Syntax hints:   → wi 4   ∈ wcel 2142  𝒫 cpw 4555  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-pw 4557  df-sn 4583  df-pr 4585

This theorem is referenced by:  unipw  5417  canth2  9102  pwfir  9261  unifpw  9298  marypha1lem  9379  infpwfidom  9984  ackbij1lem4  10178  acsfn  17691  sylow2a  19659  dissnref  23588  dissnlocfin  23589  locfindis  23590  txdis  23692  txdis1cn  23695  symgtgp  24166  1no  27903  bday0  27904  bday0b  27906  bday1  27907  cutneg  27909  cutlt  28025  oncutlt  28357  n0bday  28445  n0fincut  28448  bdayn0p1  28462  zcuts  28500  twocut  28516  addhalfcut  28552  dispcmp  34156  esumcst  34360  cntnevol  34525  coinflippvt  34782  onsucsuccmpi  36803  topdifinffinlem  37841  pclfinN  40524  lpirlnr  43694  unipwrVD  45407  unipwr  45408  salexct  46908  salexct3  46916  salgencntex  46917  salgensscntex  46918  sge0tsms  46954  sge0cl  46955  sge0sup  46965  isgrtri  48565  lincvalsng  49038  snlindsntor  49093