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 2961
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 2958 . . 3 (∀𝑥𝐴 𝜓 → (𝑥𝐴𝜓))
31, 2syl 17 . 2 (𝜑 → (𝑥𝐴𝜓))
43imp 444 1 ((𝜑𝑥𝐴) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946
This theorem is referenced by:  r19.21be  2962  rspec2  2963  rspec3  2964  ralxfr2d  4912  mptex2  6424  f1oresrab  6435  isoselem  6631  boxcutc  7993  xpf1o  8163  fineqvlem  8215  indexfi  8315  dffi3  8378  suppr  8418  supiso  8422  infpr  8450  ordtypelem9  8472  brwdom3  8528  xpwdomg  8531  ixpiunwdom  8537  infxpenc2lem1  8880  hsmexlem4  9289  gchina  9559  wunom  9580  prcdnq  9853  prnmax  9855  dedekind  10238  dedekindle  10239  monoord2  12872  limsupgre  14256  limsupbnd1  14257  limsupbnd2  14258  climmpt2  14348  rlimcld2  14353  rlimmptrcl  14382  lo1mptrcl  14396  o1mptrcl  14397  climsup  14444  sumpr  14521  sumtp  14522  fsum2dlem  14545  fsumiun  14597  fprod2dlem  14754  iserodd  15587  vdwlem1  15732  vdwlem6  15737  vdwnnlem3  15748  imasvscafn  16244  fuciso  16682  evlfcl  16909  yonedainv  16968  acsmapd  17225  prdsmndd  17370  psgnunilem5  17960  gsummpt1n0  18410  dprdspan  18472  ablfaclem2  18531  srgi  18557  srgrz  18572  srglz  18573  issrngd  18909  psrbaglesupp  19416  psrbagcon  19419  psrass1lem  19425  evlslem2  19560  mpfind  19584  gsumsmonply1  19721  gsummoncoe1  19722  evl1gsummon  19777  frgpcyg  19970  frlmgsum  20159  uvcresum  20180  cpmatmcllem  20571  neiptoptop  20983  neiptopnei  20984  ordtrest2lem  21055  cncmp  21243  1stckgenlem  21404  ptcld  21464  dfac14  21469  txcnp  21471  ptcnplem  21472  ptcnp  21473  ptcn  21478  pthaus  21489  xkococnlem  21510  xkococn  21511  cnmpt11  21514  cnmpt1t  21516  cnmpt12  21518  cnmptkp  21531  cnmptk1  21532  cnmptkk  21534  cnmptk1p  21536  cnmptk2  21537  cnmpt2k  21539  xpstopnlem1  21660  cnpflfi  21850  ptcmplem2  21904  cnextcn  21918  cnextfres1  21919  cnmpt1plusg  21938  cnmpt2plusg  21939  cnmpt1vsca  22044  cnmpt2vsca  22045  ustfilxp  22063  utoptop  22085  restutop  22088  restutopopn  22089  ucncn  22136  cfilufg  22144  trcfilu  22145  psmet0  22160  psmettri2  22161  prdsxmetlem  22220  prdsbl  22343  prdsxmslem2  22381  psmetutop  22419  cnmpt1ds  22692  cnmpt2ds  22693  cncfmpt2ss  22765  bndth  22804  cnmpt1ip  23092  cnmpt2ip  23093  iscmet3lem2  23136  cmetcusp1  23195  rrxcph  23226  ovoliunlem1  23316  ovoliunlem3  23318  ovoliun  23319  ovoliun2  23320  ovolscalem1  23327  volfiniun  23361  uniioombllem4  23400  mbfmptcl  23449  mbfeqalem  23454  mbfres2  23457  ismbf3d  23466  mbfsup  23476  mbfinf  23477  mbflim  23480  itg1ge0  23498  itg1mulc  23516  i1fposd  23519  itg1climres  23526  mbfi1fseqlem4  23530  itg2lea  23556  itg2splitlem  23560  itg2split  23561  itg2monolem1  23562  itg2mono  23565  itg2i1fseqle  23566  itg2i1fseq  23567  itg2addlem  23570  itg2cnlem1  23573  itgeqa  23625  itgss3  23626  itgfsum  23638  itgabs  23646  itggt0  23653  dvmptcl  23767  dvmptco  23780  dvlipcn  23802  dvle  23815  dvfsumle  23829  dvfsumge  23830  dvfsumabs  23831  dvmptrecl  23832  dvfsumlem2  23835  itgparts  23855  itgsubstlem  23856  itgsubst  23857  coeeulem  24025  dgrlem  24030  dgrlb  24037  coeaddlem  24050  coecj  24079  ulmss  24196  ulmdvlem2  24200  itgulm2  24208  logtayl  24451  leibpi  24714  xrlimcnp  24740  o1cxp  24746  jensen  24760  lgambdd  24808  wilthlem2  24840  sqff1o  24953  fsumdvdscom  24956  fsumdvdsmul  24966  dchrmulcl  25019  dchrmulid2  25022  dchrinv  25031  dchrisumlem3  25225  dchrvmasumlem2  25232  ostth1  25367  ercgrg  25457  f1otrg  25796  f1otrge  25797  ubthlem2  27855  fmptcof2  29585  disjdsct  29608  fprodex01  29699  ressprs  29783  oduprs  29784  archiabl  29880  lmodslmd  29885  txomap  30029  qtophaus  30031  locfinreflem  30035  ordtrest2NEWlem  30096  lmdvg  30127  prodindf  30213  esumcl  30220  esumeq2d  30227  esumnul  30238  hasheuni  30275  esumcvg  30276  esumcvgre  30281  insiga  30328  ldsysgenld  30351  ldgenpisyslem1  30354  measvunilem  30403  measvunilem0  30404  measdivcstOLD  30415  cntmeas  30417  voliune  30420  volfiniune  30421  1stmbfm  30450  2ndmbfm  30451  omssubadd  30490  difelcarsg  30500  inelcarsg  30501  eulerpartlems  30550  eulerpartlemsv3  30551  eulerpartlemgvv  30566  dstrvprob  30661  hashreprin  30826  reprgt  30827  breprexplemc  30838  circlemeth  30846  hgt750lema  30863  tgoldbachgtd  30868  bnj93  31059  bnj518  31082  bnj1489  31250  subfacp1lem3  31290  subfacp1lem5  31292  erdszelem8  31306  ptpconn  31341  resconn  31354  cvmliftmolem2  31390  cvmlift2lem11  31421  cvmliftphtlem  31425  mclsax  31592  conway  32035  slerec  32048  fin2so  33526  poimirlem18  33557  poimirlem21  33560  mblfinlem2  33577  itgabsnc  33609  itggt0cn  33612  prdsbnd  33722  prdstotbnd  33723  prdsbnd2  33724  rrnequiv  33764  eqlkr3  34706  dih1dimatlem  36935  fnwe2lem1  37937  imo72b2  38792  rfcnnnub  39509  disjxp1  39552  fompt  39693  fvixp2  39703  dmrelrnrel  39733  fvmptelrn  39742  suplesup  39868  infxr  39896  monoord2xrv  40027  climinf  40156  climsuse  40158  mullimc  40166  limccog  40170  mullimcf  40173  limcperiod  40178  limcleqr  40194  neglimc  40197  0ellimcdiv  40199  limclner  40201  limsuppnfdlem  40251  limsupubuzlem  40262  xlimmnfvlem2  40377  xlimpnfvlem2  40381  climxlim2lem  40389  dvdivbd  40456  ioodvbdlimc1lem1  40464  dvnprodlem2  40480  iblsplit  40500  stoweidlem5  40540  stoweidlem16  40551  stoweidlem21  40556  stoweidlem24  40559  stoweidlem25  40560  stoweidlem28  40563  stoweidlem31  40566  stoweidlem41  40576  stoweidlem42  40577  stoweidlem44  40579  stoweidlem45  40580  stoweidlem48  40583  stoweidlem51  40586  stoweidlem54  40589  stoweidlem57  40592  stoweidlem60  40595  stoweidlem62  40597  stirlinglem5  40613  dirkercncflem3  40640  fourierdlem11  40653  fourierdlem12  40654  fourierdlem14  40656  fourierdlem15  40657  fourierdlem31  40673  fourierdlem34  40676  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem54  40695  fourierdlem69  40710  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem79  40720  fourierdlem80  40721  fourierdlem81  40722  fourierdlem92  40733  fourierdlem93  40734  fourierdlem94  40735  fourierdlem97  40738  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem113  40754  etransclem32  40801  subsaliuncllem  40893  sge0rpcpnf  40956  caragendifcl  41049  iinhoiicclem  41208  pimdecfgtioc  41246  issmfgtlem  41285
  Copyright terms: Public domain W3C validator