Theorem snelpwi 5337

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 4741	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
2		snex 5332	. . 3 ⊢ {𝐴} ∈ V
3	2	elpw 4543	. 2 ⊢ ({𝐴} ∈ 𝒫 𝐵 ↔ {𝐴} ⊆ 𝐵)
4	1, 3	sylibr 236	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3936  𝒫 cpw 4539  {csn 4567

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 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-pw 4541  df-sn 4568  df-pr 4570

This theorem is referenced by:  unipw  5343  canth2  8670  unifpw  8827  marypha1lem  8897  infpwfidom  9454  ackbij1lem4  9645  acsfn  16930  sylow2a  18744  dissnref  22136  dissnlocfin  22137  locfindis  22138  txdis  22240  txdis1cn  22243  symgtgp  22714  dispcmp  31123  esumcst  31322  cntnevol  31487  coinflippvt  31742  onsucsuccmpi  33791  topdifinffinlem  34631  pclfinN  37051  lpirlnr  39737  unipwrVD  41186  unipwr  41187  salexct  42637  salexct3  42645  salgencntex  42646  salgensscntex  42647  sge0tsms  42682  sge0cl  42683  sge0sup  42693  lincvalsng  44491  snlindsntor  44546