Theorem snelpwi 4912

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	|- ( A e. B -> { A } e. ~P B )

Proof of Theorem snelpwi

Step	Hyp	Ref	Expression
1		snssi 4339	. 2 |- ( A e. B -> { A } C_ B )
2		snex 4908	. . 3 |- { A } e. _V
3	2	elpw 4164	. 2 |- ( { A } e. ~P B <-> { A } C_ B )
4	1, 3	sylibr 224	1 |- ( A e. B -> { A } e. ~P B )

Syntax hints:   -> wi 4   e. wcel 1990   C_ wss 3574   ~Pcpw 4158   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-pw 4160  df-sn 4178  df-pr 4180

This theorem is referenced by:  unipw  4918  canth2  8113  unifpw  8269  marypha1lem  8339  infpwfidom  8851  ackbij1lem4  9045  acsfn  16320  sylow2a  18034  dissnref  21331  dissnlocfin  21332  locfindis  21333  txdis  21435  txdis1cn  21438  symgtgp  21905  dispcmp  29926  esumcst  30125  cntnevol  30291  coinflippvt  30546  onsucsuccmpi  32442  topdifinffinlem  33195  pclfinN  35186  lpirlnr  37687  unipwrVD  39067  unipwr  39068  salexct  40552  salexct3  40560  salgencntex  40561  salgensscntex  40562  sge0tsms  40597  sge0cl  40598  sge0sup  40608  lincvalsng  42205  snlindsntor  42260