Theorem r19.21bi 3257

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-12 2215

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3080

This theorem is used by:  r19.21be  3258  rspec2  3284  rspec3  3285  ralxfr2d  5375  fvmptelcdm  7121  fompt  7126  f1oresrab  7136  isoselem  7356  mpoexw  8099  fnwe2lem2  8156  naddsuc2  8722  boxcutc  8980  xpf1o  9169  fineqvlem  9268  indexfi  9360  dffi3  9433  suppr  9474  supiso  9478  infpr  9507  ordtypelem9  9530  brwdom3  9586  xpwdomg  9589  ixpiunwdom  9594  infxpenc2lem1  10108  hsmexlem4  10517  gchina  10794  wunom  10815  prcdnq  11088  prnmax  11090  dedekind  11483  dedekindle  11484  monoord2  14186  ccatf1  14746  limsupgre  15660  limsupbnd1  15661  limsupbnd2  15662  climmpt2  15752  rlimcld2  15757  climsup  15849  sumpr  15926  sumtp  15927  fsum2dlem  15948  fsumiun  16000  fprod2dlem  16159  iserodd  17025  vdwlem1  17171  vdwlem6  17176  vdwnnlem3  17187  imasvscafn  17721  fuciso  18165  evlfcl  18408  yonedainv  18467  oduprs  18486  acsmapd  18740  chnccats1  18811  chnccat  18812  prdsmndd  18976  psgnunilem5  19720  gsummpt1n0  20191  dprdspan  20255  ablfaclem2  20314  srgdilem  20430  srgrz  20445  srglz  20446  issrngd  21124  frgpcyg  21891  psrbaglesupp  22242  psrbagcon  22245  psrbagleadd1  22248  evlslem2  22400  mpfind  22436  psdmul  22499  ply1chr  22636  gsumsmonply1  22637  gsummoncoe1  22638  evl1gsummon  22695  cpmatmcllem  23048  neiptoptop  23461  neiptopnei  23462  ordtrest2lem  23533  cncmp  23722  1stckgenlem  23884  ptcld  23944  dfac14  23949  ptcnplem  23952  pthaus  23969  xkococnlem  23990  xkococn  23991  cnmpt2k  24019  xpstopnlem1  24140  cnpflfi  24330  ptcmplem2  24384  cnextcn  24398  cnextfres1  24399  cnmpt2plusg  24419  cnmpt2vsca  24526  ustfilxp  24544  utoptop  24565  restutop  24568  restutopopn  24569  ucncn  24615  cfilufg  24623  trcfilu  24624  psmet0  24639  psmettri2  24640  prdsxmetlem  24699  prdsbl  24822  prdsxmslem2  24860  psmetutop  24898  cnmpt2ds  25175  bndth  25291  cnmpt2ip  25581  iscmet3lem2  25625  cmetcusp1  25686  rrxcph  25725  ovoliunlem1  25835  ovoliunlem3  25837  ovoliun  25838  ovoliun2  25839  ovolscalem1  25846  volfiniun  25880  uniioombllem4  25919  mbfeqalem1  25974  mbfres2  25978  ismbf3d  25987  mbfsup  25997  mbfinf  25998  mbflim  26001  itg1ge0  26019  itg1mulc  26037  itg1climres  26047  mbfi1fseqlem4  26051  itg2lea  26077  itg2splitlem  26081  itg2split  26082  itg2monolem1  26083  itg2mono  26086  itg2i1fseqle  26087  itg2i1fseq  26088  itg2addlem  26091  itg2cnlem1  26094  itgeqa  26146  itgfsum  26159  itgabs  26167  itggt0  26176  dvlipcn  26326  dvfsumabs  26355  dvfsumlem2  26359  itgsubstlem  26380  coeeulem  26555  dgrlem  26560  dgrlb  26567  coeaddlem  26580  coecj  26609  ulmss  26736  leibpi  27282  xrlimcnp  27308  o1cxp  27314  jensen  27328  lgambdd  27376  wilthlem2  27408  sqff1o  27521  fsumdvdscom  27524  fsumdvdsmul  27534  dchrmulcl  27588  dchrmullid  27591  dchrinv  27600  dchrvmasumlem2  27837  ostth1  27972  conway  28177  lesrec  28197  ercgrg  28992  f1otrg  29460  f1otrge  29461  ubthlem2  31485  fmptcof2  33305  disjdsct  33350  fprodex01  33469  prodindf  33482  ressprs  33580  mgcf1o  33617  gsumpart  33677  suppgsumssiun  33686  archiabl  33812  lmodslmd  33818  elrgspnlem1  33856  elrgspnlem2  33857  elrgspnsubrunlem2  33862  rhmimaidl  34035  gsummoncoe1fzo  34182  ply1gsumz  34184  vietadeg1  34263  vietalem  34264  fedgmullem2  34315  fedgmul  34316  txomap  34519  qtophaus  34521  locfinreflem  34525  ordtrest2NEWlem  34607  lmdvg  34638  zrhcntr  34664  esumcl  34715  esumeq2d  34722  esumnul  34733  hasheuni  34770  esumcvg  34771  esumcvgre  34776  insiga  34823  ldsysgenld  34846  ldgenpisyslem1  34849  measvunilem  34898  measvunilem0  34899  measdivcstALTV  34911  cntmeas  34912  voliune  34915  volfiniune  34916  1stmbfm  34945  2ndmbfm  34946  omssubadd  34985  difelcarsg  34995  inelcarsg  34996  eulerpartlems  35045  eulerpartlemsv3  35046  eulerpartlemgvv  35061  dstrvprob  35157  hashreprin  35302  reprgt  35303  breprexplemc  35314  circlemeth  35322  hgt750lema  35339  tgoldbachgtd  35344  bnj93  35546  bnj518  35569  bnj1489  35739  fnrelpredd  35781  srepdf  36041  subfacp1lem3  36068  subfacp1lem5  36070  erdszelem8  36084  ptpconn  36119  resconn  36132  cvmliftmolem2  36168  cvmlift2lem11  36199  cvmliftphtlem  36203  mclsax  36455  weiunfr  37382  fin2so  38670  poimirlem18  38696  poimirlem21  38699  mblfinlem2  38716  itgabsnc  38747  itggt0cn  38748  prdsbnd  38867  prdstotbnd  38868  prdsbnd2  38869  rrnequiv  38909  eqlkr3  40298  dih1dimatlem  42526  3factsumint  43215  aks6d1c5lem2  43328  cantnf2  44467  nadd1suc  44534  imo72b2  45312  rfcnnnub  46192  disjxp1  46225  disjinfi  46346  fvixp2  46352  dmrelrnrel  46378  fvmptelcdmf  46421  suplesup  46490  infxr  46517  monoord2xrv  46632  climinf  46757  climsuse  46759  mullimc  46767  limccog  46771  mullimcf  46774  limcperiod  46779  limcleqr  46793  neglimc  46796  0ellimcdiv  46798  limclner  46800  limsuppnfdlem  46850  limsupubuzlem  46861  xlimmnfvlem2  46982  xlimpnfvlem2  46986  climxlim2lem  46994  dvdivbd  47072  ioodvbdlimc1lem1  47080  dvnprodlem2  47096  iblsplit  47115  stoweidlem5  47154  stoweidlem16  47165  stoweidlem21  47170  stoweidlem24  47173  stoweidlem25  47174  stoweidlem28  47177  stoweidlem31  47180  stoweidlem41  47190  stoweidlem42  47191  stoweidlem44  47193  stoweidlem45  47194  stoweidlem48  47197  stoweidlem51  47200  stoweidlem54  47203  stoweidlem57  47206  stoweidlem60  47209  stoweidlem62  47211  stirlinglem5  47227  dirkercncflem3  47254  fourierdlem11  47267  fourierdlem12  47268  fourierdlem14  47270  fourierdlem15  47271  fourierdlem31  47287  fourierdlem34  47290  fourierdlem41  47297  fourierdlem48  47303  fourierdlem49  47304  fourierdlem50  47305  fourierdlem54  47309  fourierdlem69  47324  fourierdlem73  47328  fourierdlem74  47329  fourierdlem75  47330  fourierdlem76  47331  fourierdlem79  47334  fourierdlem80  47335  fourierdlem81  47336  fourierdlem92  47347  fourierdlem93  47348  fourierdlem94  47349  fourierdlem97  47352  fourierdlem103  47358  fourierdlem104  47359  fourierdlem111  47366  fourierdlem113  47368  etransclem32  47415  subsaliuncllem  47506  sge0rpcpnf  47570  caragendifcl  47663  iinhoiicclem  47822  pimdecfgtioc  47864  issmfgtlem  47904  ormklocald  48025  ormkglobd  48026  chnrin  48045  tmachlem-agreesn  48096  initopropd  50504  termopropd  50505  thincciso2  50729