Theorem elpwi 4168

Description: Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.)

Assertion

Ref	Expression
elpwi	|- ( A e. ~P B -> A C_ B )

Proof of Theorem elpwi

Step	Hyp	Ref	Expression
1		elpwg 4166	. 2 |- ( A e. ~P B -> ( A e. ~P B <-> A C_ B ) )
2	1	ibi 256	1 |- ( A e. ~P B -> A C_ B )

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

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  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-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  elpwid  4170  elelpwi  4171  elpwunsn  4224  elpw2g  4827  f1opw2  6888  eldifpw  6976  iunpw  6978  f1opwfi  8270  fi0  8326  fiin  8328  marypha1lem  8339  marypha1  8340  marypha2  8345  brwdom2  8478  brwdom3  8487  r1pwss  8647  rankpwi  8686  acndom  8874  acnnum  8875  dfac12r  8968  ackbij2lem1  9041  ackbij1lem6  9047  ackbij1b  9061  isfin2-2  9141  ssfin2  9142  enfin2i  9143  compsscnvlem  9192  compssiso  9196  fin11a  9205  enfin1ai  9206  fin12  9235  fin1a2s  9236  fin1a2  9237  hsmexlem2  9249  tskwe2  9595  inttsk  9596  inatsk  9600  hashbclem  13236  pr2pwpr  13261  elss2prb  13269  qshash  14559  incexclem  14568  incexc  14569  incexc2  14570  rpnnen2lem12  14954  smupf  15200  ramval  15712  ramlb  15723  mrcflem  16266  isacs2  16314  mreacs  16319  acsfn  16320  acsfn1  16322  acsfn2  16324  sscpwex  16475  fpwipodrs  17164  isacs3lem  17166  isacs4lem  17168  isacs5lem  17169  isacs5  17172  pmtrfrn  17878  oppglsm  18057  lspf  18974  pptbas  20812  clsf  20852  mretopd  20896  neiptopuni  20934  cncls2  21077  cncls  21078  cnntr  21079  restcnrm  21166  cncmp  21195  tgcmp  21204  uncmp  21206  sscmp  21208  hauscmplem  21209  cmpfi  21211  1stcrest  21256  dis2ndc  21263  lly1stc  21299  dislly  21300  comppfsc  21335  kgentopon  21341  kgen2ss  21358  kgencn  21359  kgencn2  21360  kgencn3  21361  txcmplem2  21445  txcmp  21446  tx1stc  21453  txkgen  21455  xkopt  21458  xkococnlem  21462  xkococn  21463  kqnrmlem1  21546  kqnrmlem2  21547  hmphdis  21599  isfil2  21660  isfild  21662  fbasfip  21672  neifil  21684  trfil2  21691  trufil  21714  fixufil  21726  cfinufil  21732  fin1aufil  21736  fclscmp  21834  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem5  21860  tgpconncompeqg  21915  imasf1oxms  22294  met2ndc  22328  zdis  22619  icccmp  22628  ovolf  23250  ismbl2  23295  cmmbl  23302  nulmbl  23303  nulmbl2  23304  unmbl  23305  shftmbl  23306  voliunlem2  23319  ioombl1  23330  uniioombl  23357  sqff1o  24908  musum  24917  eengtrkg  25865  edgssv2  26090  upgrreslem  26196  umgrreslem  26197  umgrres1lem  26202  upgrres1  26205  uhgrvd00  26430  rabfodom  29344  elpwincl1  29357  fpwrelmap  29508  cmpcref  29917  pcmplfinf  29928  esumcst  30125  esumfsup  30132  esum2d  30155  dmvlsiga  30192  pwsiga  30193  sigaclci  30195  sigainb  30199  insiga  30200  pwldsys  30220  ldgenpisyslem1  30226  ldgenpisyslem3  30228  measinb  30284  measres  30285  cntmeas  30289  volmeas  30294  ddemeas  30299  dya2iocucvr  30346  sxbrsigalem1  30347  omscl  30357  omsf  30358  omsmon  30360  baselcarsg  30368  difelcarsg  30372  carsgsiga  30384  omsmeas  30385  coinflippv  30545  kur14  31198  connpconn  31217  cvmsi  31247  nulsslt  31908  nulssgt  31909  neibastop1  32354  neibastop2lem  32355  neibastop3  32357  onsucsuccmpi  32442  limsucncmpi  32444  bj-0int  33055  bj-ismooredr  33064  lindsdom  33403  ismblfin  33450  cover2  33508  sstotbnd3  33575  heibor1  33609  heibor  33620  pclvalN  35176  pclfinN  35186  pclcmpatN  35187  dochfN  36645  elrfi  37257  cmpfiiin  37260  ismrcd2  37262  isnacs3  37273  aomclem2  37625  islssfg  37640  lmhmfgsplit  37656  lnrfg  37689  acsfn1p  37769  rfovcnvf1od  38298  dssmapnvod  38314  clsk1indlem3  38341  neik0pk1imk0  38345  isotone1  38346  isotone2  38347  ntrclsneine0lem  38362  ntrclsiso  38365  ntrclsk2  38366  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  ntrclsk4  38370  ntrneix2  38391  ntrneik13  38396  ntrrn  38420  dssmapntrcls  38426  sspwtr  39048  sspwtrALT  39049  sspwtrALT2  39058  pwtrVD  39059  pwtrrVD  39060  sspwimp  39154  sspwimpVD  39155  sspwimpcf  39156  sspwimpcfVD  39157  sspwimpALT  39161  sspwimpALT2  39164  pwssfi  39211  ssnnf1octb  39382  dvdmsscn  40151  dvnmptconst  40156  dvnxpaek  40157  dvnmul  40158  dvnprodlem3  40163  ismbl3  40203  ismbl4  40210  stoweidlem57  40274  pwsal  40535  prsal  40538  intsal  40548  salexct  40552  issalnnd  40563  sge0rnre  40581  sge0tsms  40597  sge0cl  40598  sge0fsum  40604  sge0sup  40608  sge0less  40609  sge0gerp  40612  sge0resplit  40623  sge0split  40626  nnfoctbdj  40673  ismeannd  40684  psmeasure  40688  caragen0  40720  caragenunidm  40722  caragenuncl  40727  caragendifcl  40728  omeiunle  40731  carageniuncl  40737  caragensal  40739  caratheodorylem2  40741  0ome  40743  isomennd  40745  caragenel2d  40746  caragencmpl  40749  ovnf  40777  ovn02  40782  ovnsubaddlem1  40784  ovnsubaddlem2  40785  ovnsubadd  40786  hspmbl  40843  isvonmbl  40852  vonmblss2  40856  ovnsubadd2lem  40859  vonvolmbl  40875  nsssmfmbf  40987  smfresal  40995  smfpimbor1lem2  41006  sprsymrelfv  41744  lincdifsn  42213  lcosslsp  42227  lindslinindsimp1  42246  lincresunit3lem1  42268  lincresunit3lem2  42269  lincresunit3  42270  elpglem1  42454  aacllem  42547