Theorem snelpwi 5412

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  𝒫 cpw 4557  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-pw 4559  df-sn 4585  df-pr 4587

This theorem is used by:  unipw  5418  canth2  9149  pwfir  9308  unifpw  9344  marypha1lem  9425  infpwfidom  10107  ackbij1lem4  10300  acsfn  17833  sylow2a  19833  dissnref  23847  dissnlocfin  23848  locfindis  23849  txdis  23951  txdis1cn  23954  symgtgp  24425  1no  28196  bday0  28197  bday0b  28199  bday1  28200  cutneg  28202  cutlt  28318  oncutlt  28650  n0bday  28738  n0fincut  28741  bdayn0p1  28755  zcuts  28793  twocut  28809  addhalfcut  28845  dispcmp  34491  esumcst  34695  cntnevol  34861  coinflippvt  35117  onsucsuccmpi  37231  topdifinffinlem  38270  pclfinN  40957  lpirlnr  44118  unipwrVD  45813  unipwr  45814  salexct  47343  salexct3  47351  salgencntex  47352  salgensscntex  47353  sge0tsms  47389  sge0cl  47390  sge0sup  47400  tmachlem-tpopen  47950  isgrtri  49040  lincvalsng  49527  snlindsntor  49582