Theorem elpwi 4567

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 4563	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
2	1	ibi 270	1 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3902  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3919  df-pw 4562

This theorem is used by:  elpwid  4569  elelpwi  4570  elpwunsn  4648  elpw2g  5302  f1opw2  7673  eldifpw  7771  pwuncl  7773  iunpw  7774  mptcnfimad  7987  pwssfi  9175  f1opwfi  9327  fi0  9394  marypha1lem  9407  marypha1  9408  marypha2  9413  brwdom2  9549  brwdom3  9558  r1pwss  9770  rankpwi  9809  acndom  10058  acnnum  10059  dfac12r  10153  ackbij2lem1  10224  ackbij1lem6  10230  ackbij1b  10244  isfin2-2  10325  ssfin2  10326  enfin2i  10327  compsscnvlem  10376  compssiso  10380  fin11a  10389  enfin1ai  10390  fin12  10419  fin1a2s  10420  fin1a2  10421  hsmexlem2  10433  tskwe2  10786  inttsk  10787  inatsk  10791  indval0  12250  hashbclem  14521  pr2pwpr  14548  elss2prb  14557  qshash  15918  incexclem  15929  incexc  15930  incexc2  15931  rpnnen2lem12  16319  smupf  16574  ramval  17106  ramlb  17117  mrcflem  17700  isacs2  17747  mreacs  17752  acsfn  17753  acsfn1  17755  acsfn2  17757  sscpwex  17910  isacs3lem  18636  isacs4lem  18638  isacs5lem  18639  isacs5  18642  pmtrfrn  19591  oppglsm  19775  acsfn1p  20971  lspf  21164  lindsdom  22069  pptbas  23239  clsf  23279  mretopd  23323  neiptopuni  23361  cncls2  23504  cncls  23505  cnntr  23506  restcnrm  23593  cncmp  23623  tgcmp  23632  uncmp  23634  sscmp  23636  hauscmplem  23637  cmpfi  23639  1stcrest  23684  dis2ndc  23692  lly1stc  23728  dislly  23729  comppfsc  23764  kgentopon  23770  kgen2ss  23787  kgencn  23788  kgencn2  23789  kgencn3  23790  txcmplem2  23874  txcmp  23875  tx1stc  23882  txkgen  23884  xkopt  23887  xkococnlem  23891  xkococn  23892  kqnrmlem1  23975  kqnrmlem2  23976  hmphdis  24028  isfil2  24088  isfild  24090  fbasfip  24100  neifil  24112  trfil2  24119  trufil  24142  fixufil  24154  cfinufil  24160  fin1aufil  24164  fclscmp  24262  alexsubALTlem2  24280  alexsubALTlem3  24281  alexsubALTlem4  24282  ptcmplem5  24288  tgpconncompeqg  24344  imasf1oxms  24721  met2ndc  24755  zdis  25049  icccmp  25058  ovolf  25716  ismbl2  25761  cmmbl  25768  nulmbl  25769  nulmbl2  25770  unmbl  25771  shftmbl  25772  voliunlem2  25785  ioombl1  25796  uniioombl  25823  sqff1o  27426  musum  27435  nulslts  28048  nulsgts  28049  madessno  28113  oldssno  28114  newssno  28115  madebdayim  28161  eengtrkg  29451  edgssv2  29666  upgrreslem  29772  umgrreslem  29773  umgrres1lem  29778  upgrres1  29781  uhgrvd00  30002  rabfodom  32988  elpwincl1  33008  fpwrelmap  33212  esplyfval2  34083  cmpcref  34368  pcmplfinf  34379  zarclsint  34390  zarcls  34392  esumcst  34581  esumfsup  34588  esum2d  34611  dmvlsiga  34647  pwsiga  34648  sigaclci  34650  sigainb  34655  insiga  34656  pwldsys  34676  ldgenpisyslem1  34682  ldgenpisyslem3  34684  measinb  34740  measres  34741  cntmeas  34745  volmeas  34750  ddemeas  34755  dya2iocucvr  34803  sxbrsigalem1  34804  omscl  34814  omsf  34815  omsmon  34817  baselcarsg  34825  difelcarsg  34829  carsgsiga  34841  omsmeas  34842  coinflippv  35003  kur14  35803  connpconn  35822  cvmsi  35852  neibastop1  36986  neibastop2lem  36987  neibastop3  36989  onsucsuccmpi  37070  limsucncmpi  37072  bj-elpwg  37804  bj-0int  37859  bj-ismooredr  37867  ismblfin  38418  cover2  38473  sstotbnd3  38534  heibor1  38568  heibor  38579  pclvalN  40771  pclfinN  40781  pclcmpatN  40782  dochfN  42237  elrfi  43547  cmpfiiin  43550  ismrcd2  43552  isnacs3  43563  aomclem2  43904  islssfg  43919  lmhmfgsplit  43935  lnrfg  43968  dfno2  44276  rfovcnvf1od  44852  dssmapnvod  44868  neik0pk1imk0  44895  isotone2  44897  ntrclsneine0lem  44912  ntrclsiso  44915  ntrclsk2  44916  ntrclskb  44917  ntrclsk3  44918  ntrclsk13  44919  ntrclsk4  44920  ntrneix2  44941  ntrneik13  44946  ntrrn  44970  dssmapntrcls  44976  ismnushort  45133  sspwtr  45651  sspwtrALT  45652  sspwtrALT2  45653  pwtrVD  45654  pwtrrVD  45655  sspwimp  45748  sspwimpVD  45749  sspwimpcf  45750  sspwimpcfVD  45751  sspwimpALT  45755  sspwimpALT2  45758  ssnnf1octb  46034  dvdmsscn  46772  dvnmptconst  46777  dvnxpaek  46778  dvnmul  46779  dvnprodlem3  46784  ismbl3  46822  ismbl4  46829  stoweidlem57  46893  pwsal  47151  prsal  47154  intsal  47166  salexct  47170  issalnnd  47181  sge0rnre  47200  sge0tsms  47216  sge0cl  47217  sge0fsum  47223  sge0sup  47227  sge0less  47228  sge0gerp  47231  sge0resplit  47242  sge0split  47245  nnfoctbdj  47292  ismeannd  47303  psmeasure  47307  caragen0  47342  caragenunidm  47344  caragenuncl  47349  caragendifcl  47350  omeiunle  47353  carageniuncl  47359  caragensal  47361  caratheodorylem2  47363  0ome  47365  isomennd  47367  caragenel2d  47368  caragencmpl  47371  ovnf  47399  ovn02  47404  ovnsubaddlem1  47406  ovnsubaddlem2  47407  ovnsubadd  47408  hspmbl  47465  isvonmbl  47474  vonmblss2  47478  ovnsubadd2lem  47481  vonvolmbl  47497  nsssmfmbf  47615  smfresal  47624  smfpimbor1lem2  47635  sprsymrelfv  48402  prpair  48409  grtriprop  48865  lincdifsn  49362  lcosslsp  49376  lindslinindsimp1  49395  lincresunit3lem1  49417  lincresunit3lem2  49418  lincresunit3  49419  isclatd  49917  elpglem1  50645  aacllem  50780