Theorem snelpwi 5339

Description: A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.)

Assertion

Ref	Expression
snelpwi	⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Proof of Theorem snelpwi

Step	Hyp	Ref	Expression
1		snssi 4743	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
2		snex 5334	. . 3 ⊢ {𝐴} ∈ V
3	2	elpw 4545	. 2 ⊢ ({𝐴} ∈ 𝒫 𝐵 ↔ {𝐴} ⊆ 𝐵)
4	1, 3	sylibr 236	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3938  𝒫 cpw 4541  {csn 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-pw 4543  df-sn 4570  df-pr 4572

This theorem is referenced by:  unipw  5345  canth2  8672  unifpw  8829  marypha1lem  8899  infpwfidom  9456  ackbij1lem4  9647  acsfn  16932  sylow2a  18746  dissnref  22138  dissnlocfin  22139  locfindis  22140  txdis  22242  txdis1cn  22245  symgtgp  22716  dispcmp  31125  esumcst  31324  cntnevol  31489  coinflippvt  31744  onsucsuccmpi  33793  topdifinffinlem  34630  pclfinN  37038  lpirlnr  39724  unipwrVD  41173  unipwr  41174  salexct  42624  salexct3  42632  salgencntex  42633  salgensscntex  42634  sge0tsms  42669  sge0cl  42670  sge0sup  42680  lincvalsng  44478  snlindsntor  44533