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 2931
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 2928 . . 3 (∀𝑥𝐴 𝜓 → (𝑥𝐴𝜓))
31, 2syl 17 . 2 (𝜑 → (𝑥𝐴𝜓))
43imp 445 1 ((𝜑𝑥𝐴) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1989  wral 2911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-12 2046
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-ral 2916
This theorem is referenced by:  r19.21be  2932  rspec2  2933  rspec3  2934  ralxfr2d  4880  mptex2  6382  f1oresrab  6393  isoselem  6588  boxcutc  7948  xpf1o  8119  fineqvlem  8171  indexfi  8271  dffi3  8334  suppr  8374  supiso  8378  infpr  8406  ordtypelem9  8428  brwdom3  8484  xpwdomg  8487  ixpiunwdom  8493  infxpenc2lem1  8839  hsmexlem4  9248  gchina  9518  wunom  9539  prcdnq  9812  prnmax  9814  dedekind  10197  dedekindle  10198  monoord2  12827  limsupgre  14206  limsupbnd1  14207  limsupbnd2  14208  climmpt2  14298  rlimcld2  14303  rlimmptrcl  14332  lo1mptrcl  14346  o1mptrcl  14347  climsup  14394  sumpr  14471  sumtp  14472  fsum2dlem  14495  fsumiun  14547  fprod2dlem  14704  iserodd  15534  vdwlem1  15679  vdwlem6  15684  vdwnnlem3  15695  imasvscafn  16191  fuciso  16629  evlfcl  16856  yonedainv  16915  acsmapd  17172  prdsmndd  17317  psgnunilem5  17908  gsummpt1n0  18358  dprdspan  18420  ablfaclem2  18479  srgi  18505  srgrz  18520  srglz  18521  issrngd  18855  psrbaglesupp  19362  psrbagcon  19365  psrass1lem  19371  evlslem2  19506  mpfind  19530  gsumsmonply1  19667  gsummoncoe1  19668  evl1gsummon  19723  frgpcyg  19916  frlmgsum  20105  uvcresum  20126  cpmatmcllem  20517  neiptoptop  20929  neiptopnei  20930  ordtrest2lem  21001  cncmp  21189  1stckgenlem  21350  ptcld  21410  dfac14  21415  txcnp  21417  ptcnplem  21418  ptcnp  21419  ptcn  21424  pthaus  21435  xkococnlem  21456  xkococn  21457  cnmpt11  21460  cnmpt1t  21462  cnmpt12  21464  cnmptkp  21477  cnmptk1  21478  cnmptkk  21480  cnmptk1p  21482  cnmptk2  21483  cnmpt2k  21485  xpstopnlem1  21606  cnpflfi  21797  ptcmplem2  21851  cnextcn  21865  cnextfres1  21866  cnmpt1plusg  21885  cnmpt2plusg  21886  cnmpt1vsca  21991  cnmpt2vsca  21992  ustfilxp  22010  utoptop  22032  restutop  22035  restutopopn  22036  ucncn  22083  cfilufg  22091  trcfilu  22092  psmet0  22107  psmettri2  22108  prdsxmetlem  22167  prdsbl  22290  prdsxmslem2  22328  psmetutop  22366  cnmpt1ds  22639  cnmpt2ds  22640  cncfmpt2ss  22712  bndth  22751  cnmpt1ip  23040  cnmpt2ip  23041  iscmet3lem2  23084  cmetcusp1  23143  rrxcph  23174  ovoliunlem1  23264  ovoliunlem3  23266  ovoliun  23267  ovoliun2  23268  ovolscalem1  23275  volfiniun  23309  uniioombllem4  23348  mbfmptcl  23398  mbfeqalem  23403  mbfres2  23406  ismbf3d  23415  mbfsup  23425  mbfinf  23426  mbflim  23429  itg1ge0  23447  itg1mulc  23465  i1fposd  23468  itg1climres  23475  mbfi1fseqlem4  23479  itg2lea  23505  itg2splitlem  23509  itg2split  23510  itg2monolem1  23511  itg2mono  23514  itg2i1fseqle  23515  itg2i1fseq  23516  itg2addlem  23519  itg2cnlem1  23522  itgeqa  23574  itgss3  23575  itgfsum  23587  itgabs  23595  itggt0  23602  dvmptcl  23716  dvmptco  23729  dvlipcn  23751  dvle  23764  dvfsumle  23778  dvfsumge  23779  dvfsumabs  23780  dvmptrecl  23781  dvfsumlem2  23784  itgparts  23804  itgsubstlem  23805  itgsubst  23806  coeeulem  23974  dgrlem  23979  dgrlb  23986  coeaddlem  23999  coecj  24028  ulmss  24145  ulmdvlem2  24149  itgulm2  24157  logtayl  24400  leibpi  24663  xrlimcnp  24689  o1cxp  24695  jensen  24709  lgambdd  24757  wilthlem2  24789  sqff1o  24902  fsumdvdscom  24905  fsumdvdsmul  24915  dchrmulcl  24968  dchrmulid2  24971  dchrinv  24980  dchrisumlem3  25174  dchrvmasumlem2  25181  ostth1  25316  ercgrg  25406  f1otrg  25745  f1otrge  25746  ubthlem2  27711  fmptcof2  29441  disjdsct  29465  fprodex01  29556  ressprs  29640  oduprs  29641  archiabl  29737  lmodslmd  29742  txomap  29886  qtophaus  29888  locfinreflem  29892  ordtrest2NEWlem  29953  lmdvg  29984  prodindf  30070  esumcl  30077  esumeq2d  30084  esumnul  30095  hasheuni  30132  esumcvg  30133  esumcvgre  30138  insiga  30185  ldsysgenld  30208  ldgenpisyslem1  30211  measvunilem  30260  measvunilem0  30261  measdivcstOLD  30272  cntmeas  30274  voliune  30277  volfiniune  30278  1stmbfm  30307  2ndmbfm  30308  omssubadd  30347  difelcarsg  30357  inelcarsg  30358  eulerpartlems  30407  eulerpartlemsv3  30408  eulerpartlemgvv  30423  dstrvprob  30518  hashreprin  30683  reprgt  30684  breprexplemc  30695  circlemeth  30703  hgt750lema  30720  tgoldbachgtd  30725  bnj93  30918  bnj518  30941  bnj1489  31109  subfacp1lem3  31149  subfacp1lem5  31151  erdszelem8  31165  ptpconn  31200  resconn  31213  cvmliftmolem2  31249  cvmlift2lem11  31280  cvmliftphtlem  31284  mclsax  31451  conway  31894  slerec  31907  fin2so  33376  poimirlem18  33407  poimirlem21  33410  mblfinlem2  33427  itgabsnc  33459  itggt0cn  33462  prdsbnd  33572  prdstotbnd  33573  prdsbnd2  33574  rrnequiv  33614  eqlkr3  34214  dih1dimatlem  36444  fnwe2lem1  37446  imo72b2  38301  rfcnnnub  39021  disjxp1  39064  fompt  39201  fvixp2  39211  dmrelrnrel  39241  fvmptelrn  39250  suplesup  39374  infxr  39402  climinf  39644  climsuse  39646  mullimc  39654  limccog  39658  mullimcf  39661  limcperiod  39666  limcleqr  39682  neglimc  39685  0ellimcdiv  39687  limclner  39689  limsuppnfdlem  39739  limsupubuzlem  39750  dvdivbd  39907  ioodvbdlimc1lem1  39915  dvnprodlem2  39931  iblsplit  39951  stoweidlem5  39991  stoweidlem16  40002  stoweidlem21  40007  stoweidlem24  40010  stoweidlem25  40011  stoweidlem28  40014  stoweidlem31  40017  stoweidlem41  40027  stoweidlem42  40028  stoweidlem44  40030  stoweidlem45  40031  stoweidlem48  40034  stoweidlem51  40037  stoweidlem54  40040  stoweidlem57  40043  stoweidlem60  40046  stoweidlem62  40048  stirlinglem5  40064  dirkercncflem3  40091  fourierdlem11  40104  fourierdlem12  40105  fourierdlem14  40107  fourierdlem15  40108  fourierdlem31  40124  fourierdlem34  40127  fourierdlem41  40134  fourierdlem48  40140  fourierdlem49  40141  fourierdlem50  40142  fourierdlem54  40146  fourierdlem69  40161  fourierdlem73  40165  fourierdlem74  40166  fourierdlem75  40167  fourierdlem76  40168  fourierdlem79  40171  fourierdlem80  40172  fourierdlem81  40173  fourierdlem92  40184  fourierdlem93  40185  fourierdlem94  40186  fourierdlem97  40189  fourierdlem103  40195  fourierdlem104  40196  fourierdlem111  40203  fourierdlem113  40205  etransclem32  40252  subsaliuncllem  40344  sge0rpcpnf  40407  caragendifcl  40497  iinhoiicclem  40656  pimdecfgtioc  40694  issmfgtlem  40733
  Copyright terms: Public domain W3C validator