MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpwi Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 elpwg 4563 . 2 (𝐴 ∈ 𝒫 𝐵 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
21ibi 266 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wss 3910  𝒫 cpw 4560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-in 3917  df-ss 3927  df-pw 4562
This theorem is referenced by:  elpwid  4569  elelpwi  4570  elpwunsn  4644  elpw2g  5301  f1opw2  7608  eldifpw  7702  pwuncl  7704  iunpw  7705  f1opwfi  9300  fi0  9356  marypha1lem  9369  marypha1  9370  marypha2  9375  brwdom2  9509  brwdom3  9518  r1pwss  9720  rankpwi  9759  acndom  9987  acnnum  9988  dfac12r  10082  ackbij2lem1  10155  ackbij1lem6  10161  ackbij1b  10175  isfin2-2  10255  ssfin2  10256  enfin2i  10257  compsscnvlem  10306  compssiso  10310  fin11a  10319  enfin1ai  10320  fin12  10349  fin1a2s  10350  fin1a2  10351  hsmexlem2  10363  tskwe2  10709  inttsk  10710  inatsk  10714  hashbclem  14349  pr2pwpr  14378  elss2prb  14386  qshash  15712  incexclem  15721  incexc  15722  incexc2  15723  rpnnen2lem12  16107  smupf  16358  ramval  16880  ramlb  16891  mrcflem  17486  isacs2  17533  mreacs  17538  acsfn  17539  acsfn1  17541  acsfn2  17543  sscpwex  17698  isacs3lem  18431  isacs4lem  18433  isacs5lem  18434  isacs5  18437  pmtrfrn  19240  oppglsm  19424  acsfn1p  20266  lspf  20435  pptbas  22358  clsf  22399  mretopd  22443  neiptopuni  22481  cncls2  22624  cncls  22625  cnntr  22626  restcnrm  22713  cncmp  22743  tgcmp  22752  uncmp  22754  sscmp  22756  hauscmplem  22757  cmpfi  22759  1stcrest  22804  dis2ndc  22811  lly1stc  22847  dislly  22848  comppfsc  22883  kgentopon  22889  kgen2ss  22906  kgencn  22907  kgencn2  22908  kgencn3  22909  txcmplem2  22993  txcmp  22994  tx1stc  23001  txkgen  23003  xkopt  23006  xkococnlem  23010  xkococn  23011  kqnrmlem1  23094  kqnrmlem2  23095  hmphdis  23147  isfil2  23207  isfild  23209  fbasfip  23219  neifil  23231  trfil2  23238  trufil  23261  fixufil  23273  cfinufil  23279  fin1aufil  23283  fclscmp  23381  alexsubALTlem2  23399  alexsubALTlem3  23400  alexsubALTlem4  23401  ptcmplem5  23407  tgpconncompeqg  23463  imasf1oxms  23845  met2ndc  23879  zdis  24179  icccmp  24188  ovolf  24846  ismbl2  24891  cmmbl  24898  nulmbl  24899  nulmbl2  24900  unmbl  24901  shftmbl  24902  voliunlem2  24915  ioombl1  24926  uniioombl  24953  sqff1o  26531  musum  26540  nulsslt  27136  nulssgt  27137  madessno  27190  oldssno  27191  newssno  27192  madebdayim  27217  eengtrkg  27935  edgssv2  28146  upgrreslem  28252  umgrreslem  28253  umgrres1lem  28258  upgrres1  28261  uhgrvd00  28482  rabfodom  31432  elpwincl1  31453  fpwrelmap  31650  cmpcref  32431  pcmplfinf  32442  zarclsint  32453  zarcls  32455  esumcst  32662  esumfsup  32669  esum2d  32692  dmvlsiga  32728  pwsiga  32729  sigaclci  32731  sigainb  32735  insiga  32736  pwldsys  32756  ldgenpisyslem1  32762  ldgenpisyslem3  32764  measinb  32820  measres  32821  cntmeas  32825  volmeas  32830  ddemeas  32835  dya2iocucvr  32884  sxbrsigalem1  32885  omscl  32895  omsf  32896  omsmon  32898  baselcarsg  32906  difelcarsg  32910  carsgsiga  32922  omsmeas  32923  coinflippv  33083  kur14  33810  connpconn  33829  cvmsi  33859  neibastop1  34831  neibastop2lem  34832  neibastop3  34834  onsucsuccmpi  34915  limsucncmpi  34917  bj-elpwg  35523  bj-0int  35572  bj-ismooredr  35580  lindsdom  36072  ismblfin  36119  cover2  36173  sstotbnd3  36235  heibor1  36269  heibor  36280  pclvalN  38353  pclfinN  38363  pclcmpatN  38364  dochfN  39819  elrfi  41003  cmpfiiin  41006  ismrcd2  41008  isnacs3  41019  aomclem2  41368  islssfg  41383  lmhmfgsplit  41399  lnrfg  41432  dfno2  41690  rfovcnvf1od  42266  dssmapnvod  42282  neik0pk1imk0  42309  isotone2  42311  ntrclsneine0lem  42326  ntrclsiso  42329  ntrclsk2  42330  ntrclskb  42331  ntrclsk3  42332  ntrclsk13  42333  ntrclsk4  42334  ntrneix2  42355  ntrneik13  42360  ntrrn  42384  dssmapntrcls  42390  ismnushort  42571  sspwtr  43093  sspwtrALT  43094  sspwtrALT2  43095  pwtrVD  43096  pwtrrVD  43097  sspwimp  43190  sspwimpVD  43191  sspwimpcf  43192  sspwimpcfVD  43193  sspwimpALT  43197  sspwimpALT2  43200  pwssfi  43243  ssnnf1octb  43404  dvdmsscn  44167  dvnmptconst  44172  dvnxpaek  44173  dvnmul  44174  dvnprodlem3  44179  ismbl3  44217  ismbl4  44224  stoweidlem57  44288  pwsal  44546  prsal  44549  intsal  44561  salexct  44565  issalnnd  44576  sge0rnre  44595  sge0tsms  44611  sge0cl  44612  sge0fsum  44618  sge0sup  44622  sge0less  44623  sge0gerp  44626  sge0resplit  44637  sge0split  44640  nnfoctbdj  44687  ismeannd  44698  psmeasure  44702  caragen0  44737  caragenunidm  44739  caragenuncl  44744  caragendifcl  44745  omeiunle  44748  carageniuncl  44754  caragensal  44756  caratheodorylem2  44758  0ome  44760  isomennd  44762  caragenel2d  44763  caragencmpl  44766  ovnf  44794  ovn02  44799  ovnsubaddlem1  44801  ovnsubaddlem2  44802  ovnsubadd  44803  hspmbl  44860  isvonmbl  44869  vonmblss2  44873  ovnsubadd2lem  44876  vonvolmbl  44892  nsssmfmbf  45010  smfresal  45019  smfpimbor1lem2  45030  sprsymrelfv  45676  prpair  45683  isomuspgrlem2c  46012  lincdifsn  46495  lcosslsp  46509  lindslinindsimp1  46528  lincresunit3lem1  46550  lincresunit3lem2  46551  lincresunit3  46552  isclatd  46998  elpglem1  47146  aacllem  47238
  Copyright terms: Public domain W3C validator