Theorem r19.21bi 3227

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 3224	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ 𝑥 ∈ 𝐴) → 𝜓)
3	1, 2	sylan 580	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045

This theorem is referenced by:  r19.21be  3228  rspec2  3254  rspec3  3255  ralxfr2d  5360  fvmptelcdm  7067  fompt  7072  f1oresrab  7081  isoselem  7298  mpoexw  8036  naddsuc2  8642  boxcutc  8891  xpf1o  9080  fineqvlem  9185  indexfi  9287  dffi3  9358  suppr  9399  supiso  9403  infpr  9432  ordtypelem9  9455  brwdom3  9511  xpwdomg  9514  ixpiunwdom  9519  infxpenc2lem1  9948  hsmexlem4  10358  gchina  10628  wunom  10649  prcdnq  10922  prnmax  10924  dedekind  11313  dedekindle  11314  monoord2  13974  limsupgre  15423  limsupbnd1  15424  limsupbnd2  15425  climmpt2  15515  rlimcld2  15520  climsup  15612  sumpr  15690  sumtp  15691  fsum2dlem  15712  fsumiun  15763  fprod2dlem  15922  iserodd  16782  vdwlem1  16928  vdwlem6  16933  vdwnnlem3  16944  imasvscafn  17476  fuciso  17916  evlfcl  18159  yonedainv  18218  oduprs  18237  acsmapd  18489  prdsmndd  18673  psgnunilem5  19400  gsummpt1n0  19871  dprdspan  19935  ablfaclem2  19994  srgdilem  20077  srgrz  20092  srglz  20093  issrngd  20740  frgpcyg  21459  psrbaglesupp  21807  psrbagcon  21810  psrbagleadd1  21813  evlslem2  21962  mpfind  21990  psdmul  22029  ply1chr  22169  gsumsmonply1  22170  gsummoncoe1  22171  evl1gsummon  22228  cpmatmcllem  22581  neiptoptop  22994  neiptopnei  22995  ordtrest2lem  23066  cncmp  23255  1stckgenlem  23416  ptcld  23476  dfac14  23481  ptcnplem  23484  pthaus  23501  xkococnlem  23522  xkococn  23523  cnmpt2k  23551  xpstopnlem1  23672  cnpflfi  23862  ptcmplem2  23916  cnextcn  23930  cnextfres1  23931  cnmpt2plusg  23951  cnmpt2vsca  24058  ustfilxp  24076  utoptop  24098  restutop  24101  restutopopn  24102  ucncn  24148  cfilufg  24156  trcfilu  24157  psmet0  24172  psmettri2  24173  prdsxmetlem  24232  prdsbl  24355  prdsxmslem2  24393  psmetutop  24431  cnmpt2ds  24708  bndth  24833  cnmpt2ip  25124  iscmet3lem2  25168  cmetcusp1  25229  rrxcph  25268  ovoliunlem1  25379  ovoliunlem3  25381  ovoliun  25382  ovoliun2  25383  ovolscalem1  25390  volfiniun  25424  uniioombllem4  25463  mbfeqalem1  25518  mbfres2  25522  ismbf3d  25531  mbfsup  25541  mbfinf  25542  mbflim  25545  itg1ge0  25563  itg1mulc  25581  itg1climres  25591  mbfi1fseqlem4  25595  itg2lea  25621  itg2splitlem  25625  itg2split  25626  itg2monolem1  25627  itg2mono  25630  itg2i1fseqle  25631  itg2i1fseq  25632  itg2addlem  25635  itg2cnlem1  25638  itgeqa  25691  itgfsum  25704  itgabs  25712  itggt0  25721  dvlipcn  25875  dvfsumabs  25905  dvfsumlem2  25909  dvfsumlem2OLD  25910  itgsubstlem  25931  coeeulem  26105  dgrlem  26110  dgrlb  26117  coeaddlem  26130  coecj  26160  coecjOLD  26162  ulmss  26282  leibpi  26828  xrlimcnp  26854  o1cxp  26861  jensen  26875  lgambdd  26923  wilthlem2  26955  sqff1o  27068  fsumdvdscom  27071  fsumdvdsmul  27081  fsumdvdsmulOLD  27083  dchrmulcl  27136  dchrmullid  27139  dchrinv  27148  dchrvmasumlem2  27385  ostth1  27520  conway  27687  slerec  27707  ercgrg  28420  f1otrg  28774  f1otrge  28775  ubthlem2  30773  fmptcof2  32554  disjdsct  32599  fprodex01  32723  prodindf  32759  ccatf1  32843  ressprs  32863  mgcf1o  32902  chnccats1  32914  gsumpart  32970  archiabl  33125  lmodslmd  33130  elrgspnlem1  33166  elrgspnlem2  33167  elrgspnsubrunlem2  33172  rhmimaidl  33376  gsummoncoe1fzo  33536  ply1gsumz  33537  fedgmullem2  33599  fedgmul  33600  txomap  33797  qtophaus  33799  locfinreflem  33803  ordtrest2NEWlem  33885  lmdvg  33916  zrhcntr  33942  esumcl  33993  esumeq2d  34000  esumnul  34011  hasheuni  34048  esumcvg  34049  esumcvgre  34054  insiga  34100  ldsysgenld  34123  ldgenpisyslem1  34126  measvunilem  34175  measvunilem0  34176  measdivcstALTV  34188  cntmeas  34189  voliune  34192  volfiniune  34193  1stmbfm  34224  2ndmbfm  34225  omssubadd  34264  difelcarsg  34274  inelcarsg  34275  eulerpartlems  34324  eulerpartlemsv3  34325  eulerpartlemgvv  34340  dstrvprob  34436  hashreprin  34584  reprgt  34585  breprexplemc  34596  circlemeth  34604  hgt750lema  34621  tgoldbachgtd  34626  bnj93  34826  bnj518  34849  bnj1489  35019  fnrelpredd  35052  subfacp1lem3  35142  subfacp1lem5  35144  erdszelem8  35158  ptpconn  35193  resconn  35206  cvmliftmolem2  35242  cvmlift2lem11  35273  cvmliftphtlem  35277  mclsax  35529  weiunfr  36428  fin2so  37574  poimirlem18  37605  poimirlem21  37608  mblfinlem2  37625  itgabsnc  37656  itggt0cn  37657  prdsbnd  37760  prdstotbnd  37761  prdsbnd2  37762  rrnequiv  37802  eqlkr3  39067  dih1dimatlem  41296  3factsumint  41986  aks6d1c5lem2  42099  fnwe2lem1  43012  cantnf2  43287  nadd1suc  43354  imo72b2  44134  rfcnnnub  45003  disjxp1  45036  disjinfi  45159  fvixp2  45166  dmrelrnrel  45193  fvmptelcdmf  45237  suplesup  45308  infxr  45336  monoord2xrv  45452  climinf  45577  climsuse  45579  mullimc  45587  limccog  45591  mullimcf  45594  limcperiod  45599  limcleqr  45615  neglimc  45618  0ellimcdiv  45620  limclner  45622  limsuppnfdlem  45672  limsupubuzlem  45683  xlimmnfvlem2  45804  xlimpnfvlem2  45808  climxlim2lem  45816  dvdivbd  45894  ioodvbdlimc1lem1  45902  dvnprodlem2  45918  iblsplit  45937  stoweidlem5  45976  stoweidlem16  45987  stoweidlem21  45992  stoweidlem24  45995  stoweidlem25  45996  stoweidlem28  45999  stoweidlem31  46002  stoweidlem41  46012  stoweidlem42  46013  stoweidlem44  46015  stoweidlem45  46016  stoweidlem48  46019  stoweidlem51  46022  stoweidlem54  46025  stoweidlem57  46028  stoweidlem60  46031  stoweidlem62  46033  stirlinglem5  46049  dirkercncflem3  46076  fourierdlem11  46089  fourierdlem12  46090  fourierdlem14  46092  fourierdlem15  46093  fourierdlem31  46109  fourierdlem34  46112  fourierdlem41  46119  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem54  46131  fourierdlem69  46146  fourierdlem73  46150  fourierdlem74  46151  fourierdlem75  46152  fourierdlem76  46153  fourierdlem79  46156  fourierdlem80  46157  fourierdlem81  46158  fourierdlem92  46169  fourierdlem93  46170  fourierdlem94  46171  fourierdlem97  46174  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  fourierdlem113  46190  etransclem32  46237  subsaliuncllem  46328  sge0rpcpnf  46392  caragendifcl  46485  iinhoiicclem  46644  pimdecfgtioc  46686  issmfgtlem  46726  ormklocald  46845  ormkglobd  46846  initopropd  49205  termopropd  49206  thincciso2  49417