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 3203
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 11-Jun-2023.)
Hypothesis
Ref Expression
r19.21bi.1 (𝜑 → ∀𝑥𝐴 𝜓)
Assertion
Ref Expression
r19.21bi ((𝜑𝑥𝐴) → 𝜓)

Proof of Theorem r19.21bi
StepHypRef Expression
1 r19.21bi.1 . 2 (𝜑 → ∀𝑥𝐴 𝜓)
2 rspa 3201 . 2 ((∀𝑥𝐴 𝜓𝑥𝐴) → 𝜓)
31, 2sylan 583 1 ((𝜑𝑥𝐴) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2115  wral 3133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-12 2179
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3138
This theorem is referenced by:  r19.21be  3204  rspec2  3205  rspec3  3206  ralxfr2d  5298  fvmptelrn  6868  f1oresrab  6880  isoselem  7087  mpoexw  7772  boxcutc  8501  xpf1o  8676  fineqvlem  8729  indexfi  8829  dffi3  8892  suppr  8932  supiso  8936  infpr  8964  ordtypelem9  8987  brwdom3  9043  xpwdomg  9046  ixpiunwdom  9051  infxpenc2lem1  9443  hsmexlem4  9849  gchina  10119  wunom  10140  prcdnq  10413  prnmax  10415  dedekind  10801  dedekindle  10802  monoord2  13406  limsupgre  14838  limsupbnd1  14839  limsupbnd2  14840  climmpt2  14930  rlimcld2  14935  climsup  15026  sumpr  15103  sumtp  15104  fsum2dlem  15125  fsumiun  15176  fprod2dlem  15334  iserodd  16170  vdwlem1  16315  vdwlem6  16320  vdwnnlem3  16331  imasvscafn  16810  fuciso  17245  evlfcl  17472  yonedainv  17531  acsmapd  17788  prdsmndd  17944  psgnunilem5  18622  gsummpt1n0  19085  dprdspan  19149  ablfaclem2  19208  srgi  19261  srgrz  19276  srglz  19277  issrngd  19632  psrbaglesupp  20148  psrbagcon  20151  evlslem2  20292  mpfind  20320  gsumsmonply1  20471  gsummoncoe1  20472  evl1gsummon  20528  frgpcyg  20720  cpmatmcllem  21326  neiptoptop  21739  neiptopnei  21740  ordtrest2lem  21811  cncmp  22000  1stckgenlem  22161  ptcld  22221  dfac14  22226  ptcnplem  22229  pthaus  22246  xkococnlem  22267  xkococn  22268  cnmpt2k  22296  xpstopnlem1  22417  cnpflfi  22607  ptcmplem2  22661  cnextcn  22675  cnextfres1  22676  cnmpt2plusg  22696  cnmpt2vsca  22803  ustfilxp  22821  utoptop  22843  restutop  22846  restutopopn  22847  ucncn  22894  cfilufg  22902  trcfilu  22903  psmet0  22918  psmettri2  22919  prdsxmetlem  22978  prdsbl  23101  prdsxmslem2  23139  psmetutop  23177  cnmpt2ds  23451  bndth  23566  cnmpt2ip  23855  iscmet3lem2  23899  cmetcusp1  23960  rrxcph  23999  ovoliunlem1  24109  ovoliunlem3  24111  ovoliun  24112  ovoliun2  24113  ovolscalem1  24120  volfiniun  24154  uniioombllem4  24193  mbfeqalem1  24248  mbfres2  24252  ismbf3d  24261  mbfsup  24271  mbfinf  24272  mbflim  24275  itg1ge0  24293  itg1mulc  24311  itg1climres  24321  mbfi1fseqlem4  24325  itg2lea  24351  itg2splitlem  24355  itg2split  24356  itg2monolem1  24357  itg2mono  24360  itg2i1fseqle  24361  itg2i1fseq  24362  itg2addlem  24365  itg2cnlem1  24368  itgeqa  24420  itgfsum  24433  itgabs  24441  itggt0  24450  dvlipcn  24600  dvfsumabs  24629  dvfsumlem2  24633  itgsubstlem  24654  coeeulem  24824  dgrlem  24829  dgrlb  24836  coeaddlem  24849  coecj  24878  ulmss  24995  leibpi  25531  xrlimcnp  25557  o1cxp  25563  jensen  25577  lgambdd  25625  wilthlem2  25657  sqff1o  25770  fsumdvdscom  25773  fsumdvdsmul  25783  dchrmulcl  25836  dchrmulid2  25839  dchrinv  25848  dchrvmasumlem2  26085  ostth1  26220  ercgrg  26314  f1otrg  26668  f1otrge  26669  ubthlem2  28657  fmptcof2  30413  disjdsct  30449  fprodex01  30552  ccatf1  30636  ressprs  30653  oduprs  30654  archiabl  30859  lmodslmd  30864  fedgmullem2  31086  fedgmul  31087  txomap  31158  qtophaus  31160  locfinreflem  31164  ordtrest2NEWlem  31222  lmdvg  31253  prodindf  31339  esumcl  31346  esumeq2d  31353  esumnul  31364  hasheuni  31401  esumcvg  31402  esumcvgre  31407  insiga  31453  ldsysgenld  31476  ldgenpisyslem1  31479  measvunilem  31528  measvunilem0  31529  measdivcstALTV  31541  cntmeas  31542  voliune  31545  volfiniune  31546  1stmbfm  31575  2ndmbfm  31576  omssubadd  31615  difelcarsg  31625  inelcarsg  31626  eulerpartlems  31675  eulerpartlemsv3  31676  eulerpartlemgvv  31691  dstrvprob  31786  hashreprin  31948  reprgt  31949  breprexplemc  31960  circlemeth  31968  hgt750lema  31985  tgoldbachgtd  31990  bnj93  32192  bnj518  32215  bnj1489  32385  subfacp1lem3  32486  subfacp1lem5  32488  erdszelem8  32502  ptpconn  32537  resconn  32550  cvmliftmolem2  32586  cvmlift2lem11  32617  cvmliftphtlem  32621  mclsax  32873  conway  33321  slerec  33334  fin2so  34989  poimirlem18  35020  poimirlem21  35023  mblfinlem2  35040  itgabsnc  35071  itggt0cn  35072  prdsbnd  35176  prdstotbnd  35177  prdsbnd2  35178  rrnequiv  35218  eqlkr3  36342  dih1dimatlem  38570  3factsumint  39261  fnwe2lem1  39910  imo72b2  40797  rfcnnnub  41585  disjxp1  41623  fompt  41744  disjinfi  41745  fvixp2  41752  dmrelrnrel  41781  suplesup  41897  infxr  41925  monoord2xrv  42049  climinf  42174  climsuse  42176  mullimc  42184  limccog  42188  mullimcf  42191  limcperiod  42196  limcleqr  42212  neglimc  42215  0ellimcdiv  42217  limclner  42219  limsuppnfdlem  42269  limsupubuzlem  42280  xlimmnfvlem2  42401  xlimpnfvlem2  42405  climxlim2lem  42413  dvdivbd  42491  ioodvbdlimc1lem1  42499  dvnprodlem2  42515  iblsplit  42534  stoweidlem5  42573  stoweidlem16  42584  stoweidlem21  42589  stoweidlem24  42592  stoweidlem25  42593  stoweidlem28  42596  stoweidlem31  42599  stoweidlem41  42609  stoweidlem42  42610  stoweidlem44  42612  stoweidlem45  42613  stoweidlem48  42616  stoweidlem51  42619  stoweidlem54  42622  stoweidlem57  42625  stoweidlem60  42628  stoweidlem62  42630  stirlinglem5  42646  dirkercncflem3  42673  fourierdlem11  42686  fourierdlem12  42687  fourierdlem14  42689  fourierdlem15  42690  fourierdlem31  42706  fourierdlem34  42709  fourierdlem41  42716  fourierdlem48  42722  fourierdlem49  42723  fourierdlem50  42724  fourierdlem54  42728  fourierdlem69  42743  fourierdlem73  42747  fourierdlem74  42748  fourierdlem75  42749  fourierdlem76  42750  fourierdlem79  42753  fourierdlem80  42754  fourierdlem81  42755  fourierdlem92  42766  fourierdlem93  42767  fourierdlem94  42768  fourierdlem97  42771  fourierdlem103  42777  fourierdlem104  42778  fourierdlem111  42785  fourierdlem113  42787  etransclem32  42834  subsaliuncllem  42923  sge0rpcpnf  42986  caragendifcl  43079  iinhoiicclem  43238  pimdecfgtioc  43276  issmfgtlem  43315
  Copyright terms: Public domain W3C validator