Theorem snelpwi 5411

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  𝒫 cpw 4556  {csn 4583

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 5390

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 3896  df-un 4151  df-pw 4558  df-sn 4584  df-pr 4586

This theorem is used by:  unipw  5417  canth2  9150  pwfir  9309  unifpw  9345  marypha1lem  9426  infpwfidom  10108  ackbij1lem4  10301  acsfn  17834  sylow2a  19834  dissnref  23848  dissnlocfin  23849  locfindis  23850  txdis  23952  txdis1cn  23955  symgtgp  24426  1no  28197  bday0  28198  bday0b  28200  bday1  28201  cutneg  28203  cutlt  28319  oncutlt  28651  n0bday  28739  n0fincut  28742  bdayn0p1  28756  zcuts  28794  twocut  28810  addhalfcut  28846  dispcmp  34534  esumcst  34738  cntnevol  34904  coinflippvt  35160  onsucsuccmpi  37274  topdifinffinlem  38314  pclfinN  41001  lpirlnr  44163  unipwrVD  45858  unipwr  45859  salexct  47388  salexct3  47396  salgencntex  47397  salgensscntex  47398  sge0tsms  47434  sge0cl  47435  sge0sup  47445  tmachlem-tpopen  47995  isgrtri  49085  lincvalsng  49572  snlindsntor  49627