Theorem snelpwi 5419

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 5418	. 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 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-pw 4559  df-sn 4585  df-pr 4587

This theorem is used by:  unipw  5425  canth2  9129  pwfir  9287  unifpw  9323  marypha1lem  9404  infpwfidom  10032  ackbij1lem4  10225  acsfn  17748  sylow2a  19747  dissnref  23755  dissnlocfin  23756  locfindis  23757  txdis  23859  txdis1cn  23862  symgtgp  24333  1no  28076  bday0  28077  bday0b  28079  bday1  28080  cutneg  28082  cutlt  28198  oncutlt  28530  n0bday  28618  n0fincut  28621  bdayn0p1  28635  zcuts  28673  twocut  28689  addhalfcut  28725  dispcmp  34370  esumcst  34574  cntnevol  34740  coinflippvt  34997  onsucsuccmpi  37063  topdifinffinlem  38102  pclfinN  40774  lpirlnr  43959  unipwrVD  45655  unipwr  45656  salexct  47163  salexct3  47171  salgencntex  47172  salgensscntex  47173  sge0tsms  47209  sge0cl  47210  sge0sup  47220  tmachlem-tpopen  47770  isgrtri  48860  lincvalsng  49347  snlindsntor  49402