Theorem snelpwi 5401

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

Syntax hints:   → wi 4   ∈ wcel 2114  𝒫 cpw 4556  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-pw 4558  df-sn 4583  df-pr 4585

This theorem is referenced by:  unipw  5407  canth2  9072  pwfir  9231  unifpw  9269  marypha1lem  9350  infpwfidom  9952  ackbij1lem4  10146  acsfn  17596  sylow2a  19565  dissnref  23489  dissnlocfin  23490  locfindis  23491  txdis  23593  txdis1cn  23596  symgtgp  24067  1no  27823  bday0  27824  bday0b  27826  bday1  27827  cutneg  27829  cutlt  27945  oncutlt  28277  n0bday  28365  n0fincut  28368  bdayn0p1  28382  zcuts  28420  twocut  28436  addhalfcut  28472  dispcmp  34043  esumcst  34247  cntnevol  34412  coinflippvt  34669  onsucsuccmpi  36665  topdifinffinlem  37629  pclfinN  40305  lpirlnr  43503  unipwrVD  45216  unipwr  45217  salexct  46721  salexct3  46729  salgencntex  46730  salgensscntex  46731  sge0tsms  46767  sge0cl  46768  sge0sup  46778  isgrtri  48332  lincvalsng  48805  snlindsntor  48860