Theorem snelpwi 5426

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

Syntax hints:   → wi 4   ∈ wcel 2149  𝒫 cpw 4567  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-pw 4569  df-sn 4595  df-pr 4597

This theorem is referenced by:  unipw  5432  canth2  9117  pwfir  9275  unifpw  9311  marypha1lem  9392  infpwfidom  10011  ackbij1lem4  10204  acsfn  17714  sylow2a  19688  dissnref  23653  dissnlocfin  23654  locfindis  23655  txdis  23757  txdis1cn  23760  symgtgp  24231  1no  27968  bday0  27969  bday0b  27971  bday1  27972  cutneg  27974  cutlt  28090  oncutlt  28422  n0bday  28510  n0fincut  28513  bdayn0p1  28527  zcuts  28565  twocut  28581  addhalfcut  28617  dispcmp  34193  esumcst  34397  cntnevol  34562  coinflippvt  34819  onsucsuccmpi  36842  topdifinffinlem  37880  pclfinN  40563  lpirlnr  43735  unipwrVD  45431  unipwr  45432  salexct  46939  salexct3  46947  salgencntex  46948  salgensscntex  46949  sge0tsms  46985  sge0cl  46986  sge0sup  46996  isgrtri  48596  lincvalsng  49080  snlindsntor  49135