Theorem elpwid 3990

Description: An element of a power class is a subclass. Deduction form of elpwi 3989. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
elpwid.1	|- ( ph -> A e. ~P B )

Assertion

Ref	Expression
elpwid	|- ( ph -> A C_ B )

Proof of Theorem elpwid

Step	Hyp	Ref	Expression
1		elpwid.1	. 2 |- ( ph -> A e. ~P B )
2		elpwi 3989	. 2 |- ( A e. ~P B -> A C_ B )
3	1, 2	syl 17	1 |- ( ph -> A C_ B )

Syntax hints:   -> wi 4   e. wcel 1869   C_ wss 3437   ~Pcpw 3980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-in 3444  df-ss 3451  df-pw 3982

This theorem is referenced by:  fopwdom  7684  ssenen  7750  fival  7930  dffi2  7941  elfiun  7948  tskwe  8387  acndom2  8487  fodomfi2  8493  infpwfien  8495  dfac12lem2  8576  ackbij1lem9  8660  ackbij1lem10  8661  ackbij1lem11  8662  ackbij1lem16  8667  ackbij2lem3  8673  cfss  8697  fin23lem7  8748  fin23lem11  8749  enfin2i  8753  isf32lem8  8792  isf34lem4  8809  isf34lem7  8811  isf34lem6  8812  isfin1-3  8818  fin1a2lem13  8844  ttukeylem6  8946  uzssz  11180  elfzoelz  11922  ackbijnn  13879  incexclem  13887  smuval2  14449  smupvallem  14450  smueqlem  14457  ramub1lem1  14977  ramub1lem2  14978  restid2  15322  mress  15492  mrcuni  15520  mreexexlem4d  15546  mreexexd  15547  mreexdomd  15548  acsfn  15558  isdrs2  16177  ipodrsima  16404  isacs3lem  16405  acsfiindd  16416  lagsubg2  16871  cntzrcl  16974  sylow1lem2  17244  sylow1lem3  17245  sylow1lem4  17246  sylow2alem2  17263  sylow2a  17264  lsmpropd  17320  lssacs  18183  lssacsex  18360  lbsextlem2  18375  lbsextlem3  18376  lbsextlem4  18377  elocv  19223  ppttop  20014  epttop  20016  clsval2  20057  mretopd  20100  neiss2  20109  neiptopnei  20140  ordtbas  20200  subbascn  20262  discmp  20405  uncmp  20410  concompcon  20439  1stcfb  20452  2ndcdisj  20463  restnlly  20489  nllyrest  20493  nllyidm  20496  cldllycmp  20502  1stckgenlem  20560  dfac14  20625  xkoccn  20626  txnlly  20644  txkgen  20659  xkopt  20662  xkoco2cn  20665  xkoinjcn  20694  tgqtop  20719  nrmhmph  20801  fbelss  20840  fbssfi  20844  infil  20870  alexsubALTlem3  21056  alexsubALTlem4  21057  ustssxp  21211  trust  21236  utopsnneiplem  21254  blssm  21425  blin2  21436  metustss  21558  metustfbas  21564  metust  21565  psmetutop  21574  restmetu  21577  icccmplem2  21833  cncfrss  21915  cncfrss2  21916  bndth  21978  lebnum  21987  ovolicc2  22468  vitalilem5  22562  i1fd  22631  dvbsss  22849  perfdvf  22850  plybss  23140  wilthlem2  23986  f1otrg  24893  uhgrass  25025  umgrass  25038  usgrass  25080  eupath2  25700  ubthlem1  26504  elpwdifcl  28150  elpwiuncl  28151  ssnnssfz  28367  indf1ofs  28849  esumval  28869  esumel  28870  gsumesum  28882  esumlub  28883  esumpcvgval  28901  esumcvg  28909  elsigass  28949  ispisys2  28977  sigapildsyslem  28985  sigapildsys  28986  ldgenpisys  28990  dynkin  28991  rossspw  28993  srossspw  29000  ddemeas  29061  br2base  29093  sxbrsigalem0  29095  dya2iocucvr  29108  sxbrsigalem2  29110  sxbrsiga  29114  oms0  29127  omssubadd  29130  omssubaddOLD  29134  carsguni  29142  elcarsgss  29143  carsggect  29152  omsmeas  29157  omsmeasOLD  29158  eulerpartlemgvv  29211  coinfliplem  29313  ballotlemfmpn  29329  cvmliftmolem2  30007  cvmlift3lem8  30051  neibastop1  31014  neibastop2lem  31015  neibastop2  31016  filnetlem4  31036  cnambfre  31947  heiborlem3  32103  heiborlem5  32105  heiborlem6  32106  heiborlem10  32110  heibor  32111  mapd1o  35179  elrfi  35499  elrfirn  35500  elrfirn2  35501  ismrcd1  35503  istopclsd  35505  mrefg3  35513  aomclem2  35877  lsmfgcl  35896  lmhmfgima  35906  elmnc  35959  stoweidlem39  37764  stoweidlem50  37775  sge0resrnlem  38077  sge0iunmptlemre  38089  psmeasurelem  38131  psmeasure  38132  uhgrss  38863  umgrss  38885  usgrss  38933  uhgssALTV  39023  ssnn0ssfz  39474