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

Theorem r19.21bi 2809
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
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 . . . 4  |-  ( ph  ->  A. x  e.  A  ps )
2 df-ral 2715 . . . 4  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
31, 2sylib 196 . . 3  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4319.21bi 1804 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
54imp 429 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1367    e. wcel 1756   A.wral 2710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-ral 2715
This theorem is referenced by:  rspec2  2810  rspec3  2811  r19.21be  2812  reusv6OLD  4498  ralxfr2d  4503  f1oresrab  5870  isoselem  6027  boxcutc  7298  xpf1o  7465  fineqvlem  7519  indexfi  7611  dffi3  7673  suppr  7710  supiso  7714  ordtypelem9  7732  brwdom3  7789  xpwdomg  7792  ixpiunwdom  7798  infxpenc2lem1  8177  hsmexlem4  8590  gchina  8858  wunom  8879  prcdnq  9154  prnmax  9156  dedekind  9525  dedekindle  9526  monoord2  11829  seqshft  12566  limsupgre  12951  limsupbnd1  12952  limsupbnd2  12953  climmpt2  13043  rlimcld2  13048  rlimmptrcl  13077  lo1mptrcl  13091  o1mptrcl  13092  climsup  13139  fsum2dlem  13229  fsumiun  13276  iserodd  13894  vdwlem1  14034  vdwlem6  14039  vdwnnlem3  14050  imasvscafn  14467  fuciso  14877  evlfcl  15024  yonedainv  15083  acsmapd  15340  prdsmndd  15446  psgnunilem5  15991  dprdspan  16512  ablfaclem2  16575  srgi  16601  srgrz  16615  srglz  16616  issrngd  16924  psrbaglesupp  17412  psrbaglesuppOLD  17413  psrbagcon  17417  psrass1lem  17424  evlslem2  17572  mpfind  17597  evl1gsummon  17774  frgpcyg  17981  frlmgsumOLD  18170  frlmgsum  18171  uvcresum  18193  neiptoptop  18710  neiptopnei  18711  ordtrest2lem  18782  cncmp  18970  1stckgenlem  19101  ptcld  19161  dfac14  19166  txcnp  19168  ptcnplem  19169  ptcnp  19170  ptcn  19175  pthaus  19186  xkococnlem  19207  xkococn  19208  cnmpt11  19211  cnmpt1t  19213  cnmpt12  19215  cnmptkp  19228  cnmptk1  19229  cnmptkk  19231  cnmptk1p  19233  cnmptk2  19234  cnmpt2k  19236  xpstopnlem1  19357  cnpflfi  19547  ptcmplem2  19600  cnextcn  19614  cnextfres  19615  cnmpt1plusg  19633  cnmpt2plusg  19634  cnmpt1vsca  19743  cnmpt2vsca  19744  ustfilxp  19762  utoptop  19784  restutop  19787  restutopopn  19788  ucncn  19835  cfilufg  19843  trcfilu  19844  psmet0  19859  psmettri2  19860  prdsxmetlem  19918  prdsbl  20041  prdsxmslem2  20079  metutopOLD  20132  psmetutop  20133  cnmpt1ds  20394  cnmpt2ds  20395  cncfmpt2ss  20466  bndth  20505  cnmpt1ip  20734  cnmpt2ip  20735  iscmet3lem2  20778  cmetcusp1OLD  20838  cmetcusp1  20839  rrxcph  20871  ovoliunlem1  20960  ovoliunlem3  20962  ovoliun  20963  ovoliun2  20964  ovolscalem1  20971  volfiniun  21003  uniioombllem4  21041  mbfmptcl  21090  mbfeqalem  21095  mbfres2  21098  ismbf3d  21107  mbfsup  21117  mbfinf  21118  mbflim  21121  itg1ge0  21139  itg1mulc  21157  i1fposd  21160  itg1climres  21167  mbfi1fseqlem4  21171  itg2lea  21197  itg2splitlem  21201  itg2split  21202  itg2monolem1  21203  itg2mono  21206  itg2i1fseqle  21207  itg2i1fseq  21208  itg2addlem  21211  itg2cnlem1  21214  itgeqa  21266  itgss3  21267  itgfsum  21279  itgabs  21287  itggt0  21294  dvmptcl  21408  dvmptco  21421  dvlipcn  21441  dvle  21454  dvfsumle  21468  dvfsumge  21469  dvfsumabs  21470  dvmptrecl  21471  dvfsumlem2  21474  itgparts  21494  itgsubstlem  21495  itgsubst  21496  coeeulem  21667  dgrlem  21672  dgrlb  21679  coeaddlem  21691  coecj  21720  ulmss  21837  ulmdvlem2  21841  itgulm2  21849  logtayl  22080  leibpi  22312  xrlimcnp  22337  o1cxp  22343  jensen  22357  wilthlem2  22382  sqff1o  22495  fsumdvdscom  22500  fsumdvdsmul  22510  dchrmulcl  22563  dchrmulid2  22566  dchrinv  22575  dchrisumlem3  22715  dchrvmasumlem2  22722  ostth1  22857  tgtrisegint  22927  ercgrg  22944  f1otrg  23068  f1otrge  23069  elntg  23181  ubthlem2  24223  abrexss  25844  ofrn  25908  fmptcof2  25930  fcnvgreu  25942  disjdsct  25949  ressprs  26067  oduprs  26068  submarchi  26154  archiabl  26166  lmodslmd  26171  sumpr  26193  kerf1hrm  26243  ordtrest2NEWlem  26304  lmdvg  26335  esumcl  26438  esumeq2d  26445  esumnul  26454  hasheuni  26486  esumcvg  26487  insiga  26532  measvunilem  26578  measvunilem0  26579  measdivcstOLD  26590  cntmeas  26592  voliune  26597  volfiniune  26598  1stmbfm  26627  2ndmbfm  26628  sitgf  26685  eulerpartlems  26695  eulerpartlemsv3  26696  eulerpartgbij  26707  eulerpartlemgvv  26711  sseqf  26727  dstrvprob  26806  signsvvfval  26931  lgambdd  26975  subfacp1lem3  27022  subfacp1lem5  27024  erdszelem8  27038  ptpcon  27074  rescon  27087  cvmliftmolem2  27123  cvmlift2lem11  27154  cvmliftphtlem  27158  fprod2dlem  27442  fin2so  28369  mblfinlem2  28382  itgabsnc  28414  itggt0cn  28417  prdsbnd  28645  prdstotbnd  28646  prdsbnd2  28647  rrnequiv  28687  fnwe2lem1  29356  rfcnnnub  29711  climinf  29732  climsuse  29734  stoweidlem5  29753  stoweidlem16  29764  stoweidlem21  29769  stoweidlem24  29772  stoweidlem25  29773  stoweidlem28  29776  stoweidlem31  29779  stoweidlem41  29789  stoweidlem42  29790  stoweidlem44  29792  stoweidlem45  29793  stoweidlem48  29796  stoweidlem51  29799  stoweidlem54  29802  stoweidlem57  29805  stoweidlem60  29808  stoweidlem62  29810  stirlinglem5  29826  bnj93  31743  bnj518  31766  bnj1489  31934  eqlkr3  32586  dih1dimatlem  34814
  Copyright terms: Public domain W3C validator