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

Theorem r19.21bi 2912
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 (𝜑 → ∀𝑥𝐴 𝜓)
Assertion
Ref Expression
r19.21bi ((𝜑𝑥𝐴) → 𝜓)

Proof of Theorem r19.21bi
StepHypRef Expression
1 r19.21bi.1 . . 3 (𝜑 → ∀𝑥𝐴 𝜓)
2 rsp 2909 . . 3 (∀𝑥𝐴 𝜓 → (𝑥𝐴𝜓))
31, 2syl 17 . 2 (𝜑 → (𝑥𝐴𝜓))
43imp 443 1 ((𝜑𝑥𝐴) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wral 2892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2032
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2897
This theorem is referenced by:  r19.21be  2913  rspec2  2914  rspec3  2915  ralxfr2d  4800  f1oresrab  6284  isoselem  6466  boxcutc  7811  xpf1o  7981  fineqvlem  8033  indexfi  8131  dffi3  8194  suppr  8234  supiso  8238  infpr  8266  ordtypelem9  8288  brwdom3  8344  xpwdomg  8347  ixpiunwdom  8353  infxpenc2lem1  8699  hsmexlem4  9108  gchina  9374  wunom  9395  prcdnq  9668  prnmax  9670  dedekind  10048  dedekindle  10049  monoord2  12646  seqshft  13616  limsupgre  14003  limsupbnd1  14004  limsupbnd2  14005  climmpt2  14095  rlimcld2  14100  rlimmptrcl  14129  lo1mptrcl  14143  o1mptrcl  14144  climsup  14191  sumpr  14264  sumtp  14265  fsum2dlem  14286  fsumiun  14337  fprod2dlem  14492  iserodd  15321  vdwlem1  15466  vdwlem6  15471  vdwnnlem3  15482  imasvscafn  15963  fuciso  16401  evlfcl  16628  yonedainv  16687  acsmapd  16944  prdsmndd  17089  psgnunilem5  17680  gsummpt1n0  18130  dprdspan  18192  ablfaclem2  18251  srgi  18277  srgrz  18292  srglz  18293  issrngd  18627  psrbaglesupp  19132  psrbagcon  19135  psrass1lem  19141  evlslem2  19276  mpfind  19300  gsumsmonply1  19437  gsummoncoe1  19438  evl1gsummon  19493  frgpcyg  19683  frlmgsum  19869  uvcresum  19890  cpmatmcllem  20281  neiptoptop  20684  neiptopnei  20685  ordtrest2lem  20756  cncmp  20944  1stckgenlem  21105  ptcld  21165  dfac14  21170  txcnp  21172  ptcnplem  21173  ptcnp  21174  ptcn  21179  pthaus  21190  xkococnlem  21211  xkococn  21212  cnmpt11  21215  cnmpt1t  21217  cnmpt12  21219  cnmptkp  21232  cnmptk1  21233  cnmptkk  21235  cnmptk1p  21237  cnmptk2  21238  cnmpt2k  21240  xpstopnlem1  21361  cnpflfi  21552  ptcmplem2  21606  cnextcn  21620  cnextfres1  21621  cnmpt1plusg  21640  cnmpt2plusg  21641  cnmpt1vsca  21746  cnmpt2vsca  21747  ustfilxp  21765  utoptop  21787  restutop  21790  restutopopn  21791  ucncn  21838  cfilufg  21846  trcfilu  21847  psmet0  21862  psmettri2  21863  prdsxmetlem  21921  prdsbl  22044  prdsxmslem2  22082  psmetutop  22120  cnmpt1ds  22382  cnmpt2ds  22383  cncfmpt2ss  22454  bndth  22493  cnmpt1ip  22769  cnmpt2ip  22770  iscmet3lem2  22813  cmetcusp1  22871  rrxcph  22902  ovoliunlem1  22991  ovoliunlem3  22993  ovoliun  22994  ovoliun2  22995  ovolscalem1  23002  volfiniun  23036  uniioombllem4  23074  mbfmptcl  23124  mbfeqalem  23129  mbfres2  23132  ismbf3d  23141  mbfsup  23151  mbfinf  23152  mbflim  23155  itg1ge0  23173  itg1mulc  23191  i1fposd  23194  itg1climres  23201  mbfi1fseqlem4  23205  itg2lea  23231  itg2splitlem  23235  itg2split  23236  itg2monolem1  23237  itg2mono  23240  itg2i1fseqle  23241  itg2i1fseq  23242  itg2addlem  23245  itg2cnlem1  23248  itgeqa  23300  itgss3  23301  itgfsum  23313  itgabs  23321  itggt0  23328  dvmptcl  23442  dvmptco  23455  dvlipcn  23475  dvle  23488  dvfsumle  23502  dvfsumge  23503  dvfsumabs  23504  dvmptrecl  23505  dvfsumlem2  23508  itgparts  23528  itgsubstlem  23529  itgsubst  23530  coeeulem  23698  dgrlem  23703  dgrlb  23710  coeaddlem  23723  coecj  23752  ulmss  23869  ulmdvlem2  23873  itgulm2  23881  logtayl  24120  leibpi  24383  xrlimcnp  24409  o1cxp  24415  jensen  24429  lgambdd  24477  wilthlem2  24509  sqff1o  24622  fsumdvdscom  24625  fsumdvdsmul  24635  dchrmulcl  24688  dchrmulid2  24691  dchrinv  24700  dchrisumlem3  24894  dchrvmasumlem2  24901  ostth1  25036  ercgrg  25127  f1otrg  25466  f1otrge  25467  ubthlem2  26914  fmptcof2  28642  disjdsct  28666  ressprs  28789  oduprs  28790  archiabl  28886  lmodslmd  28891  txomap  29032  qtophaus  29034  locfinreflem  29038  ordtrest2NEWlem  29099  lmdvg  29130  esumcl  29222  esumeq2d  29229  esumnul  29240  hasheuni  29277  esumcvg  29278  esumcvgre  29283  insiga  29330  ldsysgenld  29353  ldgenpisyslem1  29356  measvunilem  29405  measvunilem0  29406  measdivcstOLD  29417  cntmeas  29419  voliune  29422  volfiniune  29423  1stmbfm  29452  2ndmbfm  29453  omssubadd  29492  difelcarsg  29502  inelcarsg  29503  eulerpartlems  29552  eulerpartlemsv3  29553  eulerpartlemgvv  29568  dstrvprob  29663  bnj93  29990  bnj518  30013  bnj1489  30181  subfacp1lem3  30221  subfacp1lem5  30223  erdszelem8  30237  ptpcon  30272  rescon  30285  cvmliftmolem2  30321  cvmlift2lem11  30352  cvmliftphtlem  30356  mclsax  30523  fin2so  32366  poimirlem18  32397  poimirlem21  32400  mblfinlem2  32417  itgabsnc  32449  itggt0cn  32452  prdsbnd  32562  prdstotbnd  32563  prdsbnd2  32564  rrnequiv  32604  eqlkr3  33206  dih1dimatlem  35436  fnwe2lem1  36438  imo72b2  37297  rfcnnnub  38018  disjxp1  38063  mptex2  38144  fompt  38174  dmrelrnrel  38214  fvmptelrn  38223  suplesup  38297  infxr  38325  climinf  38474  climsuse  38476  mullimc  38484  limccog  38488  mullimcf  38491  limcperiod  38496  limcleqr  38512  neglimc  38515  0ellimcdiv  38517  limclner  38519  dvdivbd  38614  ioodvbdlimc1lem1  38622  dvnprodlem2  38638  iblsplit  38659  stoweidlem5  38699  stoweidlem16  38710  stoweidlem21  38715  stoweidlem24  38718  stoweidlem25  38719  stoweidlem28  38722  stoweidlem31  38725  stoweidlem41  38735  stoweidlem42  38736  stoweidlem44  38738  stoweidlem45  38739  stoweidlem48  38742  stoweidlem51  38745  stoweidlem54  38748  stoweidlem57  38751  stoweidlem60  38754  stoweidlem62  38756  stirlinglem5  38772  dirkercncflem3  38799  fourierdlem11  38812  fourierdlem12  38813  fourierdlem14  38815  fourierdlem15  38816  fourierdlem31  38832  fourierdlem34  38835  fourierdlem41  38842  fourierdlem48  38848  fourierdlem49  38849  fourierdlem50  38850  fourierdlem54  38854  fourierdlem69  38869  fourierdlem73  38873  fourierdlem74  38874  fourierdlem75  38875  fourierdlem76  38876  fourierdlem79  38879  fourierdlem80  38880  fourierdlem81  38881  fourierdlem92  38892  fourierdlem93  38893  fourierdlem94  38894  fourierdlem97  38897  fourierdlem103  38903  fourierdlem104  38904  fourierdlem111  38911  fourierdlem113  38913  etransclem32  38960  subsaliuncllem  39052  sge0rpcpnf  39115  caragendifcl  39205  iinhoiicclem  39365  pimdecfgtioc  39403  issmfgtlem  39443
  Copyright terms: Public domain W3C validator