Theorem elpwi 4543

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

Assertion

Ref	Expression
elpwi	⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)

Proof of Theorem elpwi

Step	Hyp	Ref	Expression
1		elpwg 4537	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
2	1	ibi 266	1 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3888  𝒫 cpw 4534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-pw 4536

This theorem is referenced by:  elpwid  4545  elelpwi  4546  elpwunsn  4620  elpw2g  5269  f1opw2  7533  eldifpw  7627  pwuncl  7629  iunpw  7630  f1opwfi  9132  fi0  9188  marypha1lem  9201  marypha1  9202  marypha2  9207  brwdom2  9341  brwdom3  9350  r1pwss  9551  rankpwi  9590  acndom  9816  acnnum  9817  dfac12r  9911  ackbij2lem1  9984  ackbij1lem6  9990  ackbij1b  10004  isfin2-2  10084  ssfin2  10085  enfin2i  10086  compsscnvlem  10135  compssiso  10139  fin11a  10148  enfin1ai  10149  fin12  10178  fin1a2s  10179  fin1a2  10180  hsmexlem2  10192  tskwe2  10538  inttsk  10539  inatsk  10543  hashbclem  14173  pr2pwpr  14202  elss2prb  14210  qshash  15548  incexclem  15557  incexc  15558  incexc2  15559  rpnnen2lem12  15943  smupf  16194  ramval  16718  ramlb  16729  mrcflem  17324  isacs2  17371  mreacs  17376  acsfn  17377  acsfn1  17379  acsfn2  17381  sscpwex  17536  isacs3lem  18269  isacs4lem  18271  isacs5lem  18272  isacs5  18275  pmtrfrn  19075  oppglsm  19256  acsfn1p  20076  lspf  20245  pptbas  22167  clsf  22208  mretopd  22252  neiptopuni  22290  cncls2  22433  cncls  22434  cnntr  22435  restcnrm  22522  cncmp  22552  tgcmp  22561  uncmp  22563  sscmp  22565  hauscmplem  22566  cmpfi  22568  1stcrest  22613  dis2ndc  22620  lly1stc  22656  dislly  22657  comppfsc  22692  kgentopon  22698  kgen2ss  22715  kgencn  22716  kgencn2  22717  kgencn3  22718  txcmplem2  22802  txcmp  22803  tx1stc  22810  txkgen  22812  xkopt  22815  xkococnlem  22819  xkococn  22820  kqnrmlem1  22903  kqnrmlem2  22904  hmphdis  22956  isfil2  23016  isfild  23018  fbasfip  23028  neifil  23040  trfil2  23047  trufil  23070  fixufil  23082  cfinufil  23088  fin1aufil  23092  fclscmp  23190  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALTlem4  23210  ptcmplem5  23216  tgpconncompeqg  23272  imasf1oxms  23654  met2ndc  23688  zdis  23988  icccmp  23997  ovolf  24655  ismbl2  24700  cmmbl  24707  nulmbl  24708  nulmbl2  24709  unmbl  24710  shftmbl  24711  voliunlem2  24724  ioombl1  24735  uniioombl  24762  sqff1o  26340  musum  26349  eengtrkg  27363  edgssv2  27574  upgrreslem  27680  umgrreslem  27681  umgrres1lem  27686  upgrres1  27689  uhgrvd00  27910  rabfodom  30860  elpwincl1  30883  fpwrelmap  31077  cmpcref  31809  pcmplfinf  31820  zarclsint  31831  zarcls  31833  esumcst  32040  esumfsup  32047  esum2d  32070  dmvlsiga  32106  pwsiga  32107  sigaclci  32109  sigainb  32113  insiga  32114  pwldsys  32134  ldgenpisyslem1  32140  ldgenpisyslem3  32142  measinb  32198  measres  32199  cntmeas  32203  volmeas  32208  ddemeas  32213  dya2iocucvr  32260  sxbrsigalem1  32261  omscl  32271  omsf  32272  omsmon  32274  baselcarsg  32282  difelcarsg  32286  carsgsiga  32298  omsmeas  32299  coinflippv  32459  kur14  33187  connpconn  33206  cvmsi  33236  nulsslt  34000  nulssgt  34001  madessno  34053  oldssno  34054  newssno  34055  madebdayim  34079  neibastop1  34557  neibastop2lem  34558  neibastop3  34560  onsucsuccmpi  34641  limsucncmpi  34643  bj-elpwg  35234  bj-0int  35281  bj-ismooredr  35289  lindsdom  35780  ismblfin  35827  cover2  35881  sstotbnd3  35943  heibor1  35977  heibor  35988  pclvalN  37911  pclfinN  37921  pclcmpatN  37922  dochfN  39377  elrfi  40523  cmpfiiin  40526  ismrcd2  40528  isnacs3  40539  aomclem2  40887  islssfg  40902  lmhmfgsplit  40918  lnrfg  40951  rfovcnvf1od  41619  dssmapnvod  41635  neik0pk1imk0  41664  isotone2  41666  ntrclsneine0lem  41681  ntrclsiso  41684  ntrclsk2  41685  ntrclskb  41686  ntrclsk3  41687  ntrclsk13  41688  ntrclsk4  41689  ntrneix2  41710  ntrneik13  41715  ntrrn  41739  dssmapntrcls  41745  ismnushort  41926  sspwtr  42448  sspwtrALT  42449  sspwtrALT2  42450  pwtrVD  42451  pwtrrVD  42452  sspwimp  42545  sspwimpVD  42546  sspwimpcf  42547  sspwimpcfVD  42548  sspwimpALT  42552  sspwimpALT2  42555  pwssfi  42600  ssnnf1octb  42740  dvdmsscn  43484  dvnmptconst  43489  dvnxpaek  43490  dvnmul  43491  dvnprodlem3  43496  ismbl3  43534  ismbl4  43541  stoweidlem57  43605  pwsal  43863  prsal  43866  intsal  43876  salexct  43880  issalnnd  43891  sge0rnre  43909  sge0tsms  43925  sge0cl  43926  sge0fsum  43932  sge0sup  43936  sge0less  43937  sge0gerp  43940  sge0resplit  43951  sge0split  43954  nnfoctbdj  44001  ismeannd  44012  psmeasure  44016  caragen0  44051  caragenunidm  44053  caragenuncl  44058  caragendifcl  44059  omeiunle  44062  carageniuncl  44068  caragensal  44070  caratheodorylem2  44072  0ome  44074  isomennd  44076  caragenel2d  44077  caragencmpl  44080  ovnf  44108  ovn02  44113  ovnsubaddlem1  44115  ovnsubaddlem2  44116  ovnsubadd  44117  hspmbl  44174  isvonmbl  44183  vonmblss2  44187  ovnsubadd2lem  44190  vonvolmbl  44206  nsssmfmbf  44324  smfresal  44333  smfpimbor1lem2  44344  sprsymrelfv  44957  prpair  44964  isomuspgrlem2c  45293  lincdifsn  45776  lcosslsp  45790  lindslinindsimp1  45809  lincresunit3lem1  45831  lincresunit3lem2  45832  lincresunit3  45833  isclatd  46280  elpglem1  46427  aacllem  46516