MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.21bi Structured version   Unicode version

Theorem r19.21bi 2812
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2020.)
Hypothesis
Ref Expression
r19.21bi.1  |-  ( ph  ->  A. x  e.  A  ps )
Assertion
Ref Expression
r19.21bi  |-  ( (
ph  /\  x  e.  A )  ->  ps )

Proof of Theorem r19.21bi
StepHypRef Expression
1 r19.21bi.1 . . 3  |-  ( ph  ->  A. x  e.  A  ps )
2 rsp 2809 . . 3  |-  ( A. x  e.  A  ps  ->  ( x  e.  A  ->  ps ) )
31, 2syl 16 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
43imp 429 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1804   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-12 1840
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-ral 2798
This theorem is referenced by:  r19.21be  2814  rspec2  2815  rspec3  2816  reusv6OLD  4648  ralxfr2d  4653  f1oresrab  6048  isoselem  6222  boxcutc  7514  xpf1o  7681  fineqvlem  7736  indexfi  7830  dffi3  7893  suppr  7932  supiso  7936  ordtypelem9  7954  brwdom3  8011  xpwdomg  8014  ixpiunwdom  8020  infxpenc2lem1  8399  hsmexlem4  8812  gchina  9080  wunom  9101  prcdnq  9374  prnmax  9376  dedekind  9747  dedekindle  9748  monoord2  12120  seqshft  12900  limsupgre  13286  limsupbnd1  13287  limsupbnd2  13288  climmpt2  13378  rlimcld2  13383  rlimmptrcl  13412  lo1mptrcl  13426  o1mptrcl  13427  climsup  13474  fsum2dlem  13567  fsumiun  13617  fprod2dlem  13766  iserodd  14341  vdwlem1  14481  vdwlem6  14486  vdwnnlem3  14497  imasvscafn  14916  fuciso  15323  evlfcl  15470  yonedainv  15529  acsmapd  15787  prdsmndd  15932  psgnunilem5  16498  gsummpt1n0  16971  dprdspan  17053  ablfaclem2  17116  srgi  17142  srgrz  17156  srglz  17157  issrngd  17489  psrbaglesupp  17996  psrbaglesuppOLD  17997  psrbagcon  18001  psrass1lem  18008  evlslem2  18159  mpfind  18184  gsumsmonply1  18324  gsummoncoe1  18325  evl1gsummon  18380  frgpcyg  18590  frlmgsumOLD  18779  frlmgsum  18780  uvcresum  18802  cpmatmcllem  19197  neiptoptop  19610  neiptopnei  19611  ordtrest2lem  19682  cncmp  19870  1stckgenlem  20032  ptcld  20092  dfac14  20097  txcnp  20099  ptcnplem  20100  ptcnp  20101  ptcn  20106  pthaus  20117  xkococnlem  20138  xkococn  20139  cnmpt11  20142  cnmpt1t  20144  cnmpt12  20146  cnmptkp  20159  cnmptk1  20160  cnmptkk  20162  cnmptk1p  20164  cnmptk2  20165  cnmpt2k  20167  xpstopnlem1  20288  cnpflfi  20478  ptcmplem2  20531  cnextcn  20545  cnextfres  20546  cnmpt1plusg  20564  cnmpt2plusg  20565  cnmpt1vsca  20674  cnmpt2vsca  20675  ustfilxp  20693  utoptop  20715  restutop  20718  restutopopn  20719  ucncn  20766  cfilufg  20774  trcfilu  20775  psmet0  20790  psmettri2  20791  prdsxmetlem  20849  prdsbl  20972  prdsxmslem2  21010  metutopOLD  21063  psmetutop  21064  cnmpt1ds  21325  cnmpt2ds  21326  cncfmpt2ss  21397  bndth  21436  cnmpt1ip  21665  cnmpt2ip  21666  iscmet3lem2  21709  cmetcusp1OLD  21769  cmetcusp1  21770  rrxcph  21802  ovoliunlem1  21891  ovoliunlem3  21893  ovoliun  21894  ovoliun2  21895  ovolscalem1  21902  volfiniun  21935  uniioombllem4  21973  mbfmptcl  22022  mbfeqalem  22027  mbfres2  22030  ismbf3d  22039  mbfsup  22049  mbfinf  22050  mbflim  22053  itg1ge0  22071  itg1mulc  22089  i1fposd  22092  itg1climres  22099  mbfi1fseqlem4  22103  itg2lea  22129  itg2splitlem  22133  itg2split  22134  itg2monolem1  22135  itg2mono  22138  itg2i1fseqle  22139  itg2i1fseq  22140  itg2addlem  22143  itg2cnlem1  22146  itgeqa  22198  itgss3  22199  itgfsum  22211  itgabs  22219  itggt0  22226  dvmptcl  22340  dvmptco  22353  dvlipcn  22373  dvle  22386  dvfsumle  22400  dvfsumge  22401  dvfsumabs  22402  dvmptrecl  22403  dvfsumlem2  22406  itgparts  22426  itgsubstlem  22427  itgsubst  22428  coeeulem  22599  dgrlem  22604  dgrlb  22611  coeaddlem  22624  coecj  22653  ulmss  22770  ulmdvlem2  22774  itgulm2  22782  logtayl  23019  leibpi  23251  xrlimcnp  23276  o1cxp  23282  jensen  23296  wilthlem2  23321  sqff1o  23434  fsumdvdscom  23439  fsumdvdsmul  23449  dchrmulcl  23502  dchrmulid2  23505  dchrinv  23514  dchrisumlem3  23654  dchrvmasumlem2  23661  ostth1  23796  ercgrg  23886  f1otrg  24152  f1otrge  24153  ubthlem2  25765  fmptcof2  27480  disjdsct  27499  ressprs  27621  oduprs  27622  archiabl  27720  lmodslmd  27725  sumpr  27747  txomap  27815  qtophaus  27817  locfinreflem  27821  ordtrest2NEWlem  27882  lmdvg  27913  esumcl  28021  esumeq2d  28028  esumnul  28037  hasheuni  28069  esumcvg  28070  insiga  28115  measvunilem  28161  measvunilem0  28162  measdivcstOLD  28173  cntmeas  28175  voliune  28179  volfiniune  28180  1stmbfm  28209  2ndmbfm  28210  eulerpartlems  28277  eulerpartlemsv3  28278  eulerpartlemgvv  28293  dstrvprob  28388  lgambdd  28557  subfacp1lem3  28604  subfacp1lem5  28606  erdszelem8  28620  ptpcon  28656  rescon  28669  cvmliftmolem2  28705  cvmlift2lem11  28736  cvmliftphtlem  28740  mclsax  28907  fin2so  30016  mblfinlem2  30028  itgabsnc  30060  itggt0cn  30063  prdsbnd  30265  prdstotbnd  30266  prdsbnd2  30267  rrnequiv  30307  fnwe2lem1  30972  rfcnnnub  31365  mptex2  31399  climinf  31566  climsuse  31568  mullimc  31576  limccog  31580  mullimcf  31583  limcperiod  31588  limcleqr  31604  neglimc  31607  0ellimcdiv  31609  limclner  31611  dvdivbd  31674  ioodvbdlimc1lem1  31682  dvnprodlem2  31698  iblsplit  31719  stoweidlem5  31741  stoweidlem16  31752  stoweidlem21  31757  stoweidlem24  31760  stoweidlem25  31761  stoweidlem28  31764  stoweidlem31  31767  stoweidlem41  31777  stoweidlem42  31778  stoweidlem44  31780  stoweidlem45  31781  stoweidlem48  31784  stoweidlem51  31787  stoweidlem54  31790  stoweidlem57  31793  stoweidlem60  31796  stoweidlem62  31798  stirlinglem5  31814  dirkercncflem3  31841  fourierdlem11  31854  fourierdlem12  31855  fourierdlem14  31857  fourierdlem15  31858  fourierdlem31  31874  fourierdlem34  31877  fourierdlem41  31884  fourierdlem48  31891  fourierdlem49  31892  fourierdlem50  31893  fourierdlem54  31897  fourierdlem69  31912  fourierdlem73  31916  fourierdlem74  31917  fourierdlem75  31918  fourierdlem76  31919  fourierdlem79  31922  fourierdlem80  31923  fourierdlem81  31924  fourierdlem92  31935  fourierdlem93  31936  fourierdlem94  31937  fourierdlem97  31940  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  fourierdlem113  31956  etransclem32  32003  bnj93  33789  bnj518  33812  bnj1489  33980  eqlkr3  34701  dih1dimatlem  36931  imo72b2  37797
  Copyright terms: Public domain W3C validator