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 2144  𝒫 cpw 4556  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150  df-pw 4558  df-sn 4585  df-pr 4587

This theorem is used by:  unipw  5418  canth2  9157  pwfir  9316  unifpw  9352  marypha1lem  9432  infpwfidom  10114  ackbij1lem4  10307  acsfn  17842  sylow2a  19842  dissnref  23856  dissnlocfin  23857  locfindis  23858  txdis  23960  txdis1cn  23963  symgtgp  24434  1no  28205  bday0  28206  bday0b  28208  bday1  28209  cutneg  28211  cutlt  28327  oncutlt  28659  n0bday  28747  n0fincut  28750  bdayn0p1  28764  zcuts  28802  twocut  28818  addhalfcut  28854  dispcmp  34541  esumcst  34745  cntnevol  34911  coinflippvt  35167  onsucsuccmpi  37355  topdifinffinlem  38407  pclfinN  41094  lpirlnr  44256  unipwrVD  45950  unipwr  45951  salexct  47480  salexct3  47488  salgencntex  47489  salgensscntex  47490  sge0tsms  47526  sge0cl  47527  sge0sup  47537  tmachlem-tpopen  48087  isgrtri  49177  lincvalsng  49664  snlindsntor  49719