Theorem snelpwi 5427

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  𝒫 cpw 4564  {csn 4591

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-pw 4566  df-sn 4592  df-pr 4594

This theorem is used by:  unipw  5433  canth2  9125  pwfir  9283  unifpw  9319  marypha1lem  9400  infpwfidom  10028  ackbij1lem4  10221  acsfn  17737  sylow2a  19733  dissnref  23736  dissnlocfin  23737  locfindis  23738  txdis  23840  txdis1cn  23843  symgtgp  24314  1no  28054  bday0  28055  bday0b  28057  bday1  28058  cutneg  28060  cutlt  28176  oncutlt  28508  n0bday  28596  n0fincut  28599  bdayn0p1  28613  zcuts  28651  twocut  28667  addhalfcut  28703  dispcmp  34313  esumcst  34517  cntnevol  34683  coinflippvt  34940  onsucsuccmpi  37011  topdifinffinlem  38050  pclfinN  40732  lpirlnr  43902  unipwrVD  45598  unipwr  45599  salexct  47106  salexct3  47114  salgencntex  47115  salgensscntex  47116  sge0tsms  47152  sge0cl  47153  sge0sup  47163  isgrtri  48766  lincvalsng  49253  snlindsntor  49308