Theorem elpwi 4368

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

Syntax hints:   → wi 4   ∈ wcel 2157   ⊆ wss 3776  𝒫 cpw 4358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-v 3400  df-in 3783  df-ss 3790  df-pw 4360

This theorem is referenced by:  elpwid  4370  elelpwi  4371  elpwunsn  4424  elpw2g  5026  f1opw2  7121  eldifpw  7209  iunpw  7211  f1opwfi  8512  fi0  8568  fiin  8570  marypha1lem  8581  marypha1  8582  marypha2  8587  brwdom2  8720  brwdom3  8729  r1pwss  8897  rankpwi  8936  acndom  9160  acnnum  9161  dfac12r  9256  ackbij2lem1  9329  ackbij1lem6  9335  ackbij1b  9349  isfin2-2  9429  ssfin2  9430  enfin2i  9431  compsscnvlem  9480  compssiso  9484  fin11a  9493  enfin1ai  9494  fin12  9523  fin1a2s  9524  fin1a2  9525  hsmexlem2  9537  tskwe2  9883  inttsk  9884  inatsk  9888  hashbclem  13456  pr2pwpr  13481  elss2prb  13489  qshash  14784  incexclem  14793  incexc  14794  incexc2  14795  rpnnen2lem12  15177  smupf  15422  ramval  15932  ramlb  15943  mrcflem  16474  isacs2  16521  mreacs  16526  acsfn  16527  acsfn1  16529  acsfn2  16531  sscpwex  16682  fpwipodrs  17372  isacs3lem  17374  isacs4lem  17376  isacs5lem  17377  isacs5  17380  pmtrfrn  18082  oppglsm  18261  lspf  19184  pptbas  21030  clsf  21070  mretopd  21114  neiptopuni  21152  cncls2  21295  cncls  21296  cnntr  21297  restcnrm  21384  cncmp  21413  tgcmp  21422  uncmp  21424  sscmp  21426  hauscmplem  21427  cmpfi  21429  1stcrest  21474  dis2ndc  21481  lly1stc  21517  dislly  21518  comppfsc  21553  kgentopon  21559  kgen2ss  21576  kgencn  21577  kgencn2  21578  kgencn3  21579  txcmplem2  21663  txcmp  21664  tx1stc  21671  txkgen  21673  xkopt  21676  xkococnlem  21680  xkococn  21681  kqnrmlem1  21764  kqnrmlem2  21765  hmphdis  21817  isfil2  21877  isfild  21879  fbasfip  21889  neifil  21901  trfil2  21908  trufil  21931  fixufil  21943  cfinufil  21949  fin1aufil  21953  fclscmp  22051  alexsubALTlem2  22069  alexsubALTlem3  22070  alexsubALTlem4  22071  ptcmplem5  22077  tgpconncompeqg  22132  imasf1oxms  22511  met2ndc  22545  zdis  22836  icccmp  22845  ovolf  23469  ismbl2  23514  cmmbl  23521  nulmbl  23522  nulmbl2  23523  unmbl  23524  shftmbl  23525  voliunlem2  23538  ioombl1  23549  uniioombl  23576  sqff1o  25128  musum  25137  eengtrkg  26085  edgssv2  26311  upgrreslem  26418  umgrreslem  26419  umgrres1lem  26424  upgrres1  26427  uhgrvd00  26664  rabfodom  29675  elpwincl1  29688  fpwrelmap  29841  cmpcref  30248  pcmplfinf  30259  esumcst  30456  esumfsup  30463  esum2d  30486  dmvlsiga  30523  pwsiga  30524  sigaclci  30526  sigainb  30530  insiga  30531  pwldsys  30551  ldgenpisyslem1  30557  ldgenpisyslem3  30559  measinb  30615  measres  30616  cntmeas  30620  volmeas  30625  ddemeas  30630  dya2iocucvr  30677  sxbrsigalem1  30678  omscl  30688  omsf  30689  omsmon  30691  baselcarsg  30699  difelcarsg  30703  carsgsiga  30715  omsmeas  30716  coinflippv  30876  kur14  31526  connpconn  31545  cvmsi  31575  nulsslt  32234  nulssgt  32235  neibastop1  32680  neibastop2lem  32681  neibastop3  32683  onsucsuccmpi  32764  limsucncmpi  32766  bj-0int  33368  bj-ismooredr  33377  lindsdom  33718  ismblfin  33765  cover2  33822  sstotbnd3  33888  heibor1  33922  heibor  33933  pclvalN  35672  pclfinN  35682  pclcmpatN  35683  dochfN  37138  elrfi  37760  cmpfiiin  37763  ismrcd2  37765  isnacs3  37776  aomclem2  38127  islssfg  38142  lmhmfgsplit  38158  lnrfg  38191  acsfn1p  38271  rfovcnvf1od  38799  dssmapnvod  38815  clsk1indlem3  38842  neik0pk1imk0  38846  isotone1  38847  isotone2  38848  ntrclsneine0lem  38863  ntrclsiso  38866  ntrclsk2  38867  ntrclskb  38868  ntrclsk3  38869  ntrclsk13  38870  ntrclsk4  38871  ntrneix2  38892  ntrneik13  38897  ntrrn  38921  dssmapntrcls  38927  sspwtr  39546  sspwtrALT  39547  sspwtrALT2  39553  pwtrVD  39554  pwtrrVD  39555  sspwimp  39649  sspwimpVD  39650  sspwimpcf  39651  sspwimpcfVD  39652  sspwimpALT  39656  sspwimpALT2  39659  pwssfi  39705  ssnnf1octb  39872  dvdmsscn  40632  dvnmptconst  40637  dvnxpaek  40638  dvnmul  40639  dvnprodlem3  40644  ismbl3  40683  ismbl4  40690  stoweidlem57  40754  pwsal  41015  prsal  41018  intsal  41028  salexct  41032  issalnnd  41043  sge0rnre  41061  sge0tsms  41077  sge0cl  41078  sge0fsum  41084  sge0sup  41088  sge0less  41089  sge0gerp  41092  sge0resplit  41103  sge0split  41106  nnfoctbdj  41153  ismeannd  41164  psmeasure  41168  caragen0  41203  caragenunidm  41205  caragenuncl  41210  caragendifcl  41211  omeiunle  41214  carageniuncl  41220  caragensal  41222  caratheodorylem2  41224  0ome  41226  isomennd  41228  caragenel2d  41229  caragencmpl  41232  ovnf  41260  ovn02  41265  ovnsubaddlem1  41267  ovnsubaddlem2  41268  ovnsubadd  41269  hspmbl  41326  isvonmbl  41335  vonmblss2  41339  ovnsubadd2lem  41342  vonvolmbl  41358  nsssmfmbf  41470  smfresal  41478  smfpimbor1lem2  41489  sprsymrelfv  42313  lincdifsn  42782  lcosslsp  42796  lindslinindsimp1  42815  lincresunit3lem1  42837  lincresunit3lem2  42838  lincresunit3  42839  elpglem1  43026  aacllem  43119