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

Theorem r19.21bi 2729
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 2726 . . 3  |-  ( A. x  e.  A  ps  ->  ( x  e.  A  ->  ps ) )
31, 2syl 17 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
43imp 430 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1872   A.wral 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-12 1909
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-ral 2714
This theorem is referenced by:  r19.21be  2731  rspec2  2732  rspec3  2733  ralxfr2d  4575  f1oresrab  6009  isoselem  6186  boxcutc  7515  xpf1o  7682  fineqvlem  7734  indexfi  7830  dffi3  7893  suppr  7935  supiso  7939  infpr  7967  ordtypelem9  7989  brwdom3  8045  xpwdomg  8048  ixpiunwdom  8054  infxpenc2lem1  8396  hsmexlem4  8805  gchina  9070  wunom  9091  prcdnq  9364  prnmax  9366  dedekind  9743  dedekindle  9744  monoord2  12189  seqshft  13087  limsupgre  13480  limsupgreOLD  13481  limsupbnd1  13482  limsupbnd1OLD  13483  limsupbnd2  13484  limsupbnd2OLD  13485  climmpt2  13575  rlimcld2  13580  rlimmptrcl  13609  lo1mptrcl  13623  o1mptrcl  13624  climsup  13671  sumpr  13747  sumtp  13748  fsum2dlem  13769  fsumiun  13819  fprod2dlem  13972  iserodd  14723  vdwlem1  14869  vdwlem6  14874  vdwnnlem3  14885  imasvscafn  15381  fuciso  15818  evlfcl  16045  yonedainv  16104  acsmapd  16362  prdsmndd  16507  psgnunilem5  17073  gsummpt1n0  17535  dprdspan  17598  ablfaclem2  17657  srgi  17683  srgrz  17697  srglz  17698  issrngd  18027  psrbaglesupp  18530  psrbagcon  18533  psrass1lem  18539  evlslem2  18673  mpfind  18697  gsumsmonply1  18835  gsummoncoe1  18836  evl1gsummon  18891  frgpcyg  19081  frlmgsum  19267  uvcresum  19288  cpmatmcllem  19679  neiptoptop  20084  neiptopnei  20085  ordtrest2lem  20156  cncmp  20344  1stckgenlem  20505  ptcld  20565  dfac14  20570  txcnp  20572  ptcnplem  20573  ptcnp  20574  ptcn  20579  pthaus  20590  xkococnlem  20611  xkococn  20612  cnmpt11  20615  cnmpt1t  20617  cnmpt12  20619  cnmptkp  20632  cnmptk1  20633  cnmptkk  20635  cnmptk1p  20637  cnmptk2  20638  cnmpt2k  20640  xpstopnlem1  20761  cnpflfi  20951  ptcmplem2  21005  cnextcn  21019  cnextfres1  21020  cnmpt1plusg  21039  cnmpt2plusg  21040  cnmpt1vsca  21145  cnmpt2vsca  21146  ustfilxp  21164  utoptop  21186  restutop  21189  restutopopn  21190  ucncn  21237  cfilufg  21245  trcfilu  21246  psmet0  21261  psmettri2  21262  prdsxmetlem  21320  prdsbl  21443  prdsxmslem2  21481  psmetutop  21519  cnmpt1ds  21797  cnmpt2ds  21798  cncfmpt2ss  21884  bndth  21923  cnmpt1ip  22155  cnmpt2ip  22156  iscmet3lem2  22199  cmetcusp1  22257  rrxcph  22288  ovoliunlem1  22392  ovoliunlem3  22394  ovoliun  22395  ovoliun2  22396  ovolscalem1  22403  volfiniun  22437  uniioombllem4  22481  mbfmptcl  22530  mbfeqalem  22535  mbfres2  22538  ismbf3d  22547  mbfsup  22557  mbfinf  22558  mbfinfOLD  22559  mbflim  22563  itg1ge0  22581  itg1mulc  22599  i1fposd  22602  itg1climres  22609  mbfi1fseqlem4  22613  itg2lea  22639  itg2splitlem  22643  itg2split  22644  itg2monolem1  22645  itg2mono  22648  itg2i1fseqle  22649  itg2i1fseq  22650  itg2addlem  22653  itg2cnlem1  22656  itgeqa  22708  itgss3  22709  itgfsum  22721  itgabs  22729  itggt0  22736  dvmptcl  22850  dvmptco  22863  dvlipcn  22883  dvle  22896  dvfsumle  22910  dvfsumge  22911  dvfsumabs  22912  dvmptrecl  22913  dvfsumlem2  22916  itgparts  22936  itgsubstlem  22937  itgsubst  22938  coeeulem  23115  dgrlem  23120  dgrlb  23127  coeaddlem  23140  coecj  23169  ulmss  23289  ulmdvlem2  23293  itgulm2  23301  logtayl  23542  leibpi  23805  xrlimcnp  23831  o1cxp  23837  jensen  23851  lgambdd  23899  wilthlem2  23931  sqff1o  24046  fsumdvdscom  24051  fsumdvdsmul  24061  dchrmulcl  24114  dchrmulid2  24117  dchrinv  24126  dchrisumlem3  24266  dchrvmasumlem2  24273  ostth1  24408  ercgrg  24499  f1otrg  24838  f1otrge  24839  ubthlem2  26450  fmptcof2  28200  disjdsct  28224  ressprs  28362  oduprs  28363  archiabl  28461  lmodslmd  28466  txomap  28608  qtophaus  28610  locfinreflem  28614  ordtrest2NEWlem  28675  lmdvg  28706  esumcl  28798  esumeq2d  28805  esumnul  28816  hasheuni  28853  esumcvg  28854  esumcvgre  28859  insiga  28906  ldsysgenld  28929  ldgenpisyslem1  28932  measvunilem  28981  measvunilem0  28982  measdivcstOLD  28993  cntmeas  28995  voliune  28999  volfiniune  29000  1stmbfm  29029  2ndmbfm  29030  omssubadd  29075  omssubaddOLD  29079  difelcarsg  29089  inelcarsg  29090  eulerpartlems  29140  eulerpartlemsv3  29141  eulerpartlemgvv  29156  dstrvprob  29251  bnj93  29621  bnj518  29644  bnj1489  29812  subfacp1lem3  29852  subfacp1lem5  29854  erdszelem8  29868  ptpcon  29903  rescon  29916  cvmliftmolem2  29952  cvmlift2lem11  29983  cvmliftphtlem  29987  mclsax  30154  fin2so  31839  poimirlem18  31865  poimirlem21  31868  mblfinlem2  31885  itgabsnc  31918  itggt0cn  31921  prdsbnd  32032  prdstotbnd  32033  prdsbnd2  32034  rrnequiv  32074  eqlkr3  32579  dih1dimatlem  34809  fnwe2lem1  35821  imo72b2  36532  rfcnnnub  37273  disjxp1  37327  mptex2  37336  fompt  37371  suplesup  37459  climinf  37567  climinfOLD  37568  climsuse  37570  mullimc  37579  limccog  37583  mullimcf  37586  limcperiod  37591  limcleqr  37608  neglimc  37611  0ellimcdiv  37613  limclner  37615  dvdivbd  37678  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem1OLD  37688  dvnprodlem2  37705  iblsplit  37726  stoweidlem5  37748  stoweidlem16  37759  stoweidlem21  37764  stoweidlem24  37767  stoweidlem25  37768  stoweidlem28  37771  stoweidlem31  37775  stoweidlem41  37785  stoweidlem42  37786  stoweidlem44  37788  stoweidlem45  37789  stoweidlem48  37792  stoweidlem51  37795  stoweidlem54  37798  stoweidlem57  37801  stoweidlem60  37804  stoweidlem62  37806  stoweidlem62OLD  37807  stirlinglem5  37823  dirkercncflem3  37850  fourierdlem11  37863  fourierdlem12  37864  fourierdlem14  37866  fourierdlem15  37867  fourierdlem31  37883  fourierdlem31OLD  37884  fourierdlem34  37887  fourierdlem41  37894  fourierdlem48  37901  fourierdlem49  37902  fourierdlem50  37903  fourierdlem54  37907  fourierdlem69  37922  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem76  37929  fourierdlem79  37932  fourierdlem80  37933  fourierdlem81  37934  fourierdlem92  37945  fourierdlem93  37946  fourierdlem94  37947  fourierdlem97  37950  fourierdlem103  37956  fourierdlem104  37957  fourierdlem111  37964  fourierdlem113  37966  etransclem32  38014  sge0rpcpnf  38114  caragendifcl  38186
  Copyright terms: Public domain W3C validator