Theorem r19.21bi 3230

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

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 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053

This theorem is referenced by:  r19.21be  3231  rspec2  3257  rspec3  3258  ralxfr2d  5357  fvmptelcdm  7067  fompt  7072  f1oresrab  7082  isoselem  7297  mpoexw  8032  naddsuc2  8639  boxcutc  8891  xpf1o  9079  fineqvlem  9178  indexfi  9272  dffi3  9346  suppr  9387  supiso  9391  infpr  9420  ordtypelem9  9443  brwdom3  9499  xpwdomg  9502  ixpiunwdom  9507  infxpenc2lem1  9941  hsmexlem4  10351  gchina  10622  wunom  10643  prcdnq  10916  prnmax  10918  dedekind  11308  dedekindle  11309  monoord2  13968  limsupgre  15416  limsupbnd1  15417  limsupbnd2  15418  climmpt2  15508  rlimcld2  15513  climsup  15605  sumpr  15683  sumtp  15684  fsum2dlem  15705  fsumiun  15756  fprod2dlem  15915  iserodd  16775  vdwlem1  16921  vdwlem6  16926  vdwnnlem3  16937  imasvscafn  17470  fuciso  17914  evlfcl  18157  yonedainv  18216  oduprs  18235  acsmapd  18489  chnccats1  18560  chnccat  18561  prdsmndd  18707  psgnunilem5  19435  gsummpt1n0  19906  dprdspan  19970  ablfaclem2  20029  srgdilem  20139  srgrz  20154  srglz  20155  issrngd  20800  frgpcyg  21540  psrbaglesupp  21890  psrbagcon  21893  psrbagleadd1  21896  evlslem2  22046  mpfind  22082  psdmul  22121  ply1chr  22262  gsumsmonply1  22263  gsummoncoe1  22264  evl1gsummon  22321  cpmatmcllem  22674  neiptoptop  23087  neiptopnei  23088  ordtrest2lem  23159  cncmp  23348  1stckgenlem  23509  ptcld  23569  dfac14  23574  ptcnplem  23577  pthaus  23594  xkococnlem  23615  xkococn  23616  cnmpt2k  23644  xpstopnlem1  23765  cnpflfi  23955  ptcmplem2  24009  cnextcn  24023  cnextfres1  24024  cnmpt2plusg  24044  cnmpt2vsca  24151  ustfilxp  24169  utoptop  24190  restutop  24193  restutopopn  24194  ucncn  24240  cfilufg  24248  trcfilu  24249  psmet0  24264  psmettri2  24265  prdsxmetlem  24324  prdsbl  24447  prdsxmslem2  24485  psmetutop  24523  cnmpt2ds  24800  bndth  24925  cnmpt2ip  25216  iscmet3lem2  25260  cmetcusp1  25321  rrxcph  25360  ovoliunlem1  25471  ovoliunlem3  25473  ovoliun  25474  ovoliun2  25475  ovolscalem1  25482  volfiniun  25516  uniioombllem4  25555  mbfeqalem1  25610  mbfres2  25614  ismbf3d  25623  mbfsup  25633  mbfinf  25634  mbflim  25637  itg1ge0  25655  itg1mulc  25673  itg1climres  25683  mbfi1fseqlem4  25687  itg2lea  25713  itg2splitlem  25717  itg2split  25718  itg2monolem1  25719  itg2mono  25722  itg2i1fseqle  25723  itg2i1fseq  25724  itg2addlem  25727  itg2cnlem1  25730  itgeqa  25783  itgfsum  25796  itgabs  25804  itggt0  25813  dvlipcn  25967  dvfsumabs  25997  dvfsumlem2  26001  dvfsumlem2OLD  26002  itgsubstlem  26023  coeeulem  26197  dgrlem  26202  dgrlb  26209  coeaddlem  26222  coecj  26252  coecjOLD  26254  ulmss  26374  leibpi  26920  xrlimcnp  26946  o1cxp  26953  jensen  26967  lgambdd  27015  wilthlem2  27047  sqff1o  27160  fsumdvdscom  27163  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  dchrmulcl  27228  dchrmullid  27231  dchrinv  27240  dchrvmasumlem2  27477  ostth1  27612  conway  27787  lesrec  27807  ercgrg  28601  f1otrg  28955  f1otrge  28956  ubthlem2  30959  fmptcof2  32747  disjdsct  32793  fprodex01  32917  prodindf  32955  ccatf1  33042  ressprs  33059  mgcf1o  33096  gsumpart  33157  suppgsumssiun  33166  archiabl  33292  lmodslmd  33298  elrgspnlem1  33336  elrgspnlem2  33337  elrgspnsubrunlem2  33342  rhmimaidl  33525  gsummoncoe1fzo  33690  ply1gsumz  33692  vietadeg1  33755  vietalem  33756  fedgmullem2  33808  fedgmul  33809  txomap  34012  qtophaus  34014  locfinreflem  34018  ordtrest2NEWlem  34100  lmdvg  34131  zrhcntr  34157  esumcl  34208  esumeq2d  34215  esumnul  34226  hasheuni  34263  esumcvg  34264  esumcvgre  34269  insiga  34315  ldsysgenld  34338  ldgenpisyslem1  34341  measvunilem  34390  measvunilem0  34391  measdivcstALTV  34403  cntmeas  34404  voliune  34407  volfiniune  34408  1stmbfm  34438  2ndmbfm  34439  omssubadd  34478  difelcarsg  34488  inelcarsg  34489  eulerpartlems  34538  eulerpartlemsv3  34539  eulerpartlemgvv  34554  dstrvprob  34650  hashreprin  34798  reprgt  34799  breprexplemc  34810  circlemeth  34818  hgt750lema  34835  tgoldbachgtd  34840  bnj93  35039  bnj518  35062  bnj1489  35232  fnrelpredd  35268  subfacp1lem3  35398  subfacp1lem5  35400  erdszelem8  35414  ptpconn  35449  resconn  35462  cvmliftmolem2  35498  cvmlift2lem11  35529  cvmliftphtlem  35533  mclsax  35785  weiunfr  36683  fin2so  37858  poimirlem18  37889  poimirlem21  37892  mblfinlem2  37909  itgabsnc  37940  itggt0cn  37941  prdsbnd  38044  prdstotbnd  38045  prdsbnd2  38046  rrnequiv  38086  eqlkr3  39477  dih1dimatlem  41705  3factsumint  42395  aks6d1c5lem2  42508  fnwe2lem1  43407  cantnf2  43682  nadd1suc  43749  imo72b2  44528  rfcnnnub  45396  disjxp1  45429  disjinfi  45551  fvixp2  45557  dmrelrnrel  45584  fvmptelcdmf  45628  suplesup  45698  infxr  45725  monoord2xrv  45841  climinf  45966  climsuse  45968  mullimc  45976  limccog  45980  mullimcf  45983  limcperiod  45988  limcleqr  46002  neglimc  46005  0ellimcdiv  46007  limclner  46009  limsuppnfdlem  46059  limsupubuzlem  46070  xlimmnfvlem2  46191  xlimpnfvlem2  46195  climxlim2lem  46203  dvdivbd  46281  ioodvbdlimc1lem1  46289  dvnprodlem2  46305  iblsplit  46324  stoweidlem5  46363  stoweidlem16  46374  stoweidlem21  46379  stoweidlem24  46382  stoweidlem25  46383  stoweidlem28  46386  stoweidlem31  46389  stoweidlem41  46399  stoweidlem42  46400  stoweidlem44  46402  stoweidlem45  46403  stoweidlem48  46406  stoweidlem51  46409  stoweidlem54  46412  stoweidlem57  46415  stoweidlem60  46418  stoweidlem62  46420  stirlinglem5  46436  dirkercncflem3  46463  fourierdlem11  46476  fourierdlem12  46477  fourierdlem14  46479  fourierdlem15  46480  fourierdlem31  46496  fourierdlem34  46499  fourierdlem41  46506  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem54  46518  fourierdlem69  46533  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem76  46540  fourierdlem79  46543  fourierdlem80  46544  fourierdlem81  46545  fourierdlem92  46556  fourierdlem93  46557  fourierdlem94  46558  fourierdlem97  46561  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  fourierdlem113  46577  etransclem32  46624  subsaliuncllem  46715  sge0rpcpnf  46779  caragendifcl  46872  iinhoiicclem  47031  pimdecfgtioc  47073  issmfgtlem  47113  ormklocald  47232  ormkglobd  47233  initopropd  49602  termopropd  49603  thincciso2  49814