Theorem r19.21bi 3259

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

Step	Hyp	Ref	Expression
1		r19.21bi.1	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
2		rspa 3256	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ 𝑥 ∈ 𝐴) → 𝜓)
3	1, 2	sylan 592	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3082

This theorem is used by:  r19.21be  3260  rspec2  3286  rspec3  3287  ralxfr2d  5383  fvmptelcdm  7112  fompt  7117  f1oresrab  7127  isoselem  7348  mpoexw  8081  naddsuc2  8694  boxcutc  8945  xpf1o  9134  fineqvlem  9233  indexfi  9324  dffi3  9398  suppr  9439  supiso  9443  infpr  9472  ordtypelem9  9495  brwdom3  9551  xpwdomg  9554  ixpiunwdom  9559  infxpenc2lem1  10019  hsmexlem4  10428  gchina  10699  wunom  10720  prcdnq  10993  prnmax  10995  dedekind  11388  dedekindle  11389  monoord2  14087  ccatf1  14646  limsupgre  15556  limsupbnd1  15557  limsupbnd2  15558  climmpt2  15648  rlimcld2  15653  climsup  15745  sumpr  15822  sumtp  15823  fsum2dlem  15844  fsumiun  15896  fprod2dlem  16057  iserodd  16917  vdwlem1  17063  vdwlem6  17068  vdwnnlem3  17079  imasvscafn  17613  fuciso  18057  evlfcl  18300  yonedainv  18359  oduprs  18378  acsmapd  18632  chnccats1  18703  chnccat  18704  prdsmndd  18865  psgnunilem5  19608  gsummpt1n0  20079  dprdspan  20143  ablfaclem2  20202  srgdilem  20318  srgrz  20333  srglz  20334  issrngd  21008  frgpcyg  21773  psrbaglesupp  22122  psrbagcon  22125  psrbagleadd1  22128  evlslem2  22280  mpfind  22316  psdmul  22379  ply1chr  22516  gsumsmonply1  22517  gsummoncoe1  22518  evl1gsummon  22575  cpmatmcllem  22925  neiptoptop  23338  neiptopnei  23339  ordtrest2lem  23410  cncmp  23599  1stckgenlem  23761  ptcld  23821  dfac14  23826  ptcnplem  23829  pthaus  23846  xkococnlem  23867  xkococn  23868  cnmpt2k  23896  xpstopnlem1  24017  cnpflfi  24207  ptcmplem2  24261  cnextcn  24275  cnextfres1  24276  cnmpt2plusg  24296  cnmpt2vsca  24403  ustfilxp  24421  utoptop  24442  restutop  24445  restutopopn  24446  ucncn  24492  cfilufg  24500  trcfilu  24501  psmet0  24516  psmettri2  24517  prdsxmetlem  24576  prdsbl  24699  prdsxmslem2  24737  psmetutop  24775  cnmpt2ds  25052  bndth  25168  cnmpt2ip  25458  iscmet3lem2  25502  cmetcusp1  25563  rrxcph  25602  ovoliunlem1  25712  ovoliunlem3  25714  ovoliun  25715  ovoliun2  25716  ovolscalem1  25723  volfiniun  25757  uniioombllem4  25796  mbfeqalem1  25851  mbfres2  25855  ismbf3d  25864  mbfsup  25874  mbfinf  25875  mbflim  25878  itg1ge0  25896  itg1mulc  25914  itg1climres  25924  mbfi1fseqlem4  25928  itg2lea  25954  itg2splitlem  25958  itg2split  25959  itg2monolem1  25960  itg2mono  25963  itg2i1fseqle  25964  itg2i1fseq  25965  itg2addlem  25968  itg2cnlem1  25971  itgeqa  26024  itgfsum  26037  itgabs  26045  itggt0  26054  dvlipcn  26204  dvfsumabs  26233  dvfsumlem2  26237  itgsubstlem  26258  coeeulem  26432  dgrlem  26437  dgrlb  26444  coeaddlem  26457  coecj  26486  coecjOLD  26488  ulmss  26611  leibpi  27158  xrlimcnp  27184  o1cxp  27190  jensen  27204  lgambdd  27252  wilthlem2  27284  sqff1o  27397  fsumdvdscom  27400  fsumdvdsmul  27410  dchrmulcl  27464  dchrmullid  27467  dchrinv  27476  dchrvmasumlem2  27713  ostth1  27848  conway  28023  lesrec  28043  ercgrg  28837  f1otrg  29275  f1otrge  29276  ubthlem2  31294  fmptcof2  33073  disjdsct  33119  fprodex01  33239  prodindf  33252  ressprs  33350  mgcf1o  33387  gsumpart  33447  suppgsumssiun  33456  archiabl  33582  lmodslmd  33588  elrgspnlem1  33626  elrgspnlem2  33627  elrgspnsubrunlem2  33632  rhmimaidl  33804  gsummoncoe1fzo  33951  ply1gsumz  33953  vietadeg1  34032  vietalem  34033  fedgmullem2  34084  fedgmul  34085  txomap  34288  qtophaus  34290  locfinreflem  34294  ordtrest2NEWlem  34376  lmdvg  34407  zrhcntr  34433  esumcl  34484  esumeq2d  34491  esumnul  34502  hasheuni  34539  esumcvg  34540  esumcvgre  34545  insiga  34592  ldsysgenld  34615  ldgenpisyslem1  34618  measvunilem  34667  measvunilem0  34668  measdivcstALTV  34680  cntmeas  34681  voliune  34684  volfiniune  34685  1stmbfm  34715  2ndmbfm  34716  omssubadd  34755  difelcarsg  34765  inelcarsg  34766  eulerpartlems  34815  eulerpartlemsv3  34816  eulerpartlemgvv  34831  dstrvprob  34927  hashreprin  35072  reprgt  35073  breprexplemc  35084  circlemeth  35092  hgt750lema  35109  tgoldbachgtd  35114  bnj93  35316  bnj518  35339  bnj1489  35509  fnrelpredd  35540  subfacp1lem3  35711  subfacp1lem5  35713  erdszelem8  35727  ptpconn  35762  resconn  35775  cvmliftmolem2  35811  cvmlift2lem11  35842  cvmliftphtlem  35846  mclsax  36098  weiunfr  37035  fin2so  38315  poimirlem18  38346  poimirlem21  38349  mblfinlem2  38366  itgabsnc  38397  itggt0cn  38398  prdsbnd  38502  prdstotbnd  38503  prdsbnd2  38504  rrnequiv  38544  eqlkr3  39933  dih1dimatlem  42161  3factsumint  42850  aks6d1c5lem2  42963  fnwe2lem1  43835  cantnf2  44110  nadd1suc  44177  imo72b2  44956  rfcnnnub  45814  disjxp1  45847  disjinfi  45968  fvixp2  45974  dmrelrnrel  46000  fvmptelcdmf  46043  suplesup  46113  infxr  46140  monoord2xrv  46255  climinf  46380  climsuse  46382  mullimc  46390  limccog  46394  mullimcf  46397  limcperiod  46402  limcleqr  46416  neglimc  46419  0ellimcdiv  46421  limclner  46423  limsuppnfdlem  46473  limsupubuzlem  46484  xlimmnfvlem2  46605  xlimpnfvlem2  46609  climxlim2lem  46617  dvdivbd  46695  ioodvbdlimc1lem1  46703  dvnprodlem2  46719  iblsplit  46738  stoweidlem5  46777  stoweidlem16  46788  stoweidlem21  46793  stoweidlem24  46796  stoweidlem25  46797  stoweidlem28  46800  stoweidlem31  46803  stoweidlem41  46813  stoweidlem42  46814  stoweidlem44  46816  stoweidlem45  46817  stoweidlem48  46820  stoweidlem51  46823  stoweidlem54  46826  stoweidlem57  46829  stoweidlem60  46832  stoweidlem62  46834  stirlinglem5  46850  dirkercncflem3  46877  fourierdlem11  46890  fourierdlem12  46891  fourierdlem14  46893  fourierdlem15  46894  fourierdlem31  46910  fourierdlem34  46913  fourierdlem41  46920  fourierdlem48  46926  fourierdlem49  46927  fourierdlem50  46928  fourierdlem54  46932  fourierdlem69  46947  fourierdlem73  46951  fourierdlem74  46952  fourierdlem75  46953  fourierdlem76  46954  fourierdlem79  46957  fourierdlem80  46958  fourierdlem81  46959  fourierdlem92  46970  fourierdlem93  46971  fourierdlem94  46972  fourierdlem97  46975  fourierdlem103  46981  fourierdlem104  46982  fourierdlem111  46989  fourierdlem113  46991  etransclem32  47038  subsaliuncllem  47129  sge0rpcpnf  47193  caragendifcl  47286  iinhoiicclem  47445  pimdecfgtioc  47487  issmfgtlem  47527  ormklocald  47648  ormkglobd  47649  initopropd  50078  termopropd  50079  thincciso2  50290