Theorem snelpwi 5383

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

Syntax hints:   → wi 4   ∈ wcel 2119  𝒫 cpw 4529  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-pw 4531  df-sn 4556  df-pr 4558

This theorem is referenced by:  unipw  5389  canth2  9058  pwfir  9217  unifpw  9255  marypha1lem  9336  infpwfidom  9941  ackbij1lem4  10135  acsfn  17616  sylow2a  19585  dissnref  23511  dissnlocfin  23512  locfindis  23513  txdis  23615  txdis1cn  23618  symgtgp  24089  1no  27820  bday0  27821  bday0b  27823  bday1  27824  cutneg  27826  cutlt  27942  oncutlt  28274  n0bday  28362  n0fincut  28365  bdayn0p1  28379  zcuts  28417  twocut  28433  addhalfcut  28469  dispcmp  34043  esumcst  34247  cntnevol  34412  coinflippvt  34669  onsucsuccmpi  36671  topdifinffinlem  37709  pclfinN  40392  lpirlnr  43562  unipwrVD  45275  unipwr  45276  salexct  46777  salexct3  46785  salgencntex  46786  salgensscntex  46787  sge0tsms  46823  sge0cl  46824  sge0sup  46834  isgrtri  48434  lincvalsng  48907  snlindsntor  48962