Theorem r19.21bi 3255

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

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

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 2213

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

This theorem is used by:  r19.21be  3256  rspec2  3282  rspec3  3283  ralxfr2d  5372  fvmptelcdm  7113  fompt  7118  f1oresrab  7128  isoselem  7349  mpoexw  8091  fnwe2lem2  8146  naddsuc2  8711  boxcutc  8969  xpf1o  9158  fineqvlem  9257  indexfi  9349  dffi3  9423  suppr  9464  supiso  9468  infpr  9497  ordtypelem9  9520  brwdom3  9576  xpwdomg  9579  ixpiunwdom  9584  infxpenc2lem1  10098  hsmexlem4  10507  gchina  10784  wunom  10805  prcdnq  11078  prnmax  11080  dedekind  11473  dedekindle  11474  monoord2  14176  ccatf1  14736  limsupgre  15648  limsupbnd1  15649  limsupbnd2  15650  climmpt2  15740  rlimcld2  15745  climsup  15837  sumpr  15914  sumtp  15915  fsum2dlem  15936  fsumiun  15988  fprod2dlem  16147  iserodd  17013  vdwlem1  17159  vdwlem6  17164  vdwnnlem3  17175  imasvscafn  17709  fuciso  18153  evlfcl  18396  yonedainv  18455  oduprs  18474  acsmapd  18728  chnccats1  18799  chnccat  18800  prdsmndd  18964  psgnunilem5  19708  gsummpt1n0  20179  dprdspan  20243  ablfaclem2  20302  srgdilem  20418  srgrz  20433  srglz  20434  issrngd  21112  frgpcyg  21879  psrbaglesupp  22230  psrbagcon  22233  psrbagleadd1  22236  evlslem2  22388  mpfind  22424  psdmul  22487  ply1chr  22624  gsumsmonply1  22625  gsummoncoe1  22626  evl1gsummon  22683  cpmatmcllem  23036  neiptoptop  23449  neiptopnei  23450  ordtrest2lem  23521  cncmp  23710  1stckgenlem  23872  ptcld  23932  dfac14  23937  ptcnplem  23940  pthaus  23957  xkococnlem  23978  xkococn  23979  cnmpt2k  24007  xpstopnlem1  24128  cnpflfi  24318  ptcmplem2  24372  cnextcn  24386  cnextfres1  24387  cnmpt2plusg  24407  cnmpt2vsca  24514  ustfilxp  24532  utoptop  24553  restutop  24556  restutopopn  24557  ucncn  24603  cfilufg  24611  trcfilu  24612  psmet0  24627  psmettri2  24628  prdsxmetlem  24687  prdsbl  24810  prdsxmslem2  24848  psmetutop  24886  cnmpt2ds  25163  bndth  25279  cnmpt2ip  25569  iscmet3lem2  25613  cmetcusp1  25674  rrxcph  25713  ovoliunlem1  25823  ovoliunlem3  25825  ovoliun  25826  ovoliun2  25827  ovolscalem1  25834  volfiniun  25868  uniioombllem4  25907  mbfeqalem1  25962  mbfres2  25966  ismbf3d  25975  mbfsup  25985  mbfinf  25986  mbflim  25989  itg1ge0  26007  itg1mulc  26025  itg1climres  26035  mbfi1fseqlem4  26039  itg2lea  26065  itg2splitlem  26069  itg2split  26070  itg2monolem1  26071  itg2mono  26074  itg2i1fseqle  26075  itg2i1fseq  26076  itg2addlem  26079  itg2cnlem1  26082  itgeqa  26134  itgfsum  26147  itgabs  26155  itggt0  26164  dvlipcn  26314  dvfsumabs  26343  dvfsumlem2  26347  itgsubstlem  26368  coeeulem  26543  dgrlem  26548  dgrlb  26555  coeaddlem  26568  coecj  26597  ulmss  26724  leibpi  27270  xrlimcnp  27296  o1cxp  27302  jensen  27316  lgambdd  27364  wilthlem2  27396  sqff1o  27509  fsumdvdscom  27512  fsumdvdsmul  27522  dchrmulcl  27576  dchrmullid  27579  dchrinv  27588  dchrvmasumlem2  27825  ostth1  27960  conway  28165  lesrec  28185  ercgrg  28980  f1otrg  29448  f1otrge  29449  ubthlem2  31473  fmptcof2  33251  disjdsct  33296  fprodex01  33416  prodindf  33429  ressprs  33527  mgcf1o  33564  gsumpart  33624  suppgsumssiun  33633  archiabl  33759  lmodslmd  33765  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnsubrunlem2  33809  rhmimaidl  33982  gsummoncoe1fzo  34129  ply1gsumz  34131  vietadeg1  34210  vietalem  34211  fedgmullem2  34262  fedgmul  34263  txomap  34466  qtophaus  34468  locfinreflem  34472  ordtrest2NEWlem  34554  lmdvg  34585  zrhcntr  34611  esumcl  34662  esumeq2d  34669  esumnul  34680  hasheuni  34717  esumcvg  34718  esumcvgre  34723  insiga  34770  ldsysgenld  34793  ldgenpisyslem1  34796  measvunilem  34845  measvunilem0  34846  measdivcstALTV  34858  cntmeas  34859  voliune  34862  volfiniune  34863  1stmbfm  34892  2ndmbfm  34893  omssubadd  34932  difelcarsg  34942  inelcarsg  34943  eulerpartlems  34992  eulerpartlemsv3  34993  eulerpartlemgvv  35008  dstrvprob  35104  hashreprin  35249  reprgt  35250  breprexplemc  35261  circlemeth  35269  hgt750lema  35286  tgoldbachgtd  35291  bnj93  35493  bnj518  35516  bnj1489  35686  fnrelpredd  35720  subfacp1lem3  35947  subfacp1lem5  35949  erdszelem8  35963  ptpconn  35998  resconn  36011  cvmliftmolem2  36047  cvmlift2lem11  36078  cvmliftphtlem  36082  mclsax  36334  weiunfr  37255  fin2so  38530  poimirlem18  38556  poimirlem21  38559  mblfinlem2  38576  itgabsnc  38607  itggt0cn  38608  prdsbnd  38727  prdstotbnd  38728  prdsbnd2  38729  rrnequiv  38769  eqlkr3  40158  dih1dimatlem  42386  3factsumint  43075  aks6d1c5lem2  43188  cantnf2  44326  nadd1suc  44393  imo72b2  45171  rfcnnnub  46052  disjxp1  46085  disjinfi  46206  fvixp2  46212  dmrelrnrel  46238  fvmptelcdmf  46281  suplesup  46350  infxr  46377  monoord2xrv  46492  climinf  46617  climsuse  46619  mullimc  46627  limccog  46631  mullimcf  46634  limcperiod  46639  limcleqr  46653  neglimc  46656  0ellimcdiv  46658  limclner  46660  limsuppnfdlem  46710  limsupubuzlem  46721  xlimmnfvlem2  46842  xlimpnfvlem2  46846  climxlim2lem  46854  dvdivbd  46932  ioodvbdlimc1lem1  46940  dvnprodlem2  46956  iblsplit  46975  stoweidlem5  47014  stoweidlem16  47025  stoweidlem21  47030  stoweidlem24  47033  stoweidlem25  47034  stoweidlem28  47037  stoweidlem31  47040  stoweidlem41  47050  stoweidlem42  47051  stoweidlem44  47053  stoweidlem45  47054  stoweidlem48  47057  stoweidlem51  47060  stoweidlem54  47063  stoweidlem57  47066  stoweidlem60  47069  stoweidlem62  47071  stirlinglem5  47087  dirkercncflem3  47114  fourierdlem11  47127  fourierdlem12  47128  fourierdlem14  47130  fourierdlem15  47131  fourierdlem31  47147  fourierdlem34  47150  fourierdlem41  47157  fourierdlem48  47163  fourierdlem49  47164  fourierdlem50  47165  fourierdlem54  47169  fourierdlem69  47184  fourierdlem73  47188  fourierdlem74  47189  fourierdlem75  47190  fourierdlem76  47191  fourierdlem79  47194  fourierdlem80  47195  fourierdlem81  47196  fourierdlem92  47207  fourierdlem93  47208  fourierdlem94  47209  fourierdlem97  47212  fourierdlem103  47218  fourierdlem104  47219  fourierdlem111  47226  fourierdlem113  47228  etransclem32  47275  subsaliuncllem  47366  sge0rpcpnf  47430  caragendifcl  47523  iinhoiicclem  47682  pimdecfgtioc  47724  issmfgtlem  47764  ormklocald  47885  ormkglobd  47886  chnrin  47905  tmachlem-agreesn  47956  initopropd  50350  termopropd  50351  thincciso2  50562