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 591	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080

This theorem is referenced by:  r19.21be  3258  rspec2  3284  rspec3  3285  ralxfr2d  5381  fvmptelcdm  7108  fompt  7113  f1oresrab  7123  isoselem  7339  mpoexw  8071  naddsuc2  8684  boxcutc  8935  xpf1o  9123  fineqvlem  9222  indexfi  9313  dffi3  9387  suppr  9428  supiso  9432  infpr  9461  ordtypelem9  9484  brwdom3  9540  xpwdomg  9543  ixpiunwdom  9548  infxpenc2lem1  9999  hsmexlem4  10408  gchina  10679  wunom  10700  prcdnq  10973  prnmax  10975  dedekind  11368  dedekindle  11369  monoord2  14065  limsupgre  15528  limsupbnd1  15529  limsupbnd2  15530  climmpt2  15620  rlimcld2  15625  climsup  15717  sumpr  15795  sumtp  15796  fsum2dlem  15817  fsumiun  15869  fprod2dlem  16030  iserodd  16890  vdwlem1  17036  vdwlem6  17041  vdwnnlem3  17052  imasvscafn  17586  fuciso  18030  evlfcl  18273  yonedainv  18332  oduprs  18351  acsmapd  18605  chnccats1  18676  chnccat  18677  prdsmndd  18823  psgnunilem5  19559  gsummpt1n0  20030  dprdspan  20094  ablfaclem2  20153  srgdilem  20269  srgrz  20284  srglz  20285  issrngd  20958  frgpcyg  21723  psrbaglesupp  22072  psrbagcon  22075  psrbagleadd1  22078  evlslem2  22230  mpfind  22266  psdmul  22329  ply1chr  22466  gsumsmonply1  22467  gsummoncoe1  22468  evl1gsummon  22525  cpmatmcllem  22875  neiptoptop  23288  neiptopnei  23289  ordtrest2lem  23360  cncmp  23549  1stckgenlem  23710  ptcld  23770  dfac14  23775  ptcnplem  23778  pthaus  23795  xkococnlem  23816  xkococn  23817  cnmpt2k  23845  xpstopnlem1  23966  cnpflfi  24156  ptcmplem2  24210  cnextcn  24224  cnextfres1  24225  cnmpt2plusg  24245  cnmpt2vsca  24352  ustfilxp  24370  utoptop  24391  restutop  24394  restutopopn  24395  ucncn  24441  cfilufg  24449  trcfilu  24450  psmet0  24465  psmettri2  24466  prdsxmetlem  24525  prdsbl  24648  prdsxmslem2  24686  psmetutop  24724  cnmpt2ds  25001  bndth  25117  cnmpt2ip  25407  iscmet3lem2  25451  cmetcusp1  25512  rrxcph  25551  ovoliunlem1  25661  ovoliunlem3  25663  ovoliun  25664  ovoliun2  25665  ovolscalem1  25672  volfiniun  25706  uniioombllem4  25745  mbfeqalem1  25800  mbfres2  25804  ismbf3d  25813  mbfsup  25823  mbfinf  25824  mbflim  25827  itg1ge0  25845  itg1mulc  25863  itg1climres  25873  mbfi1fseqlem4  25877  itg2lea  25903  itg2splitlem  25907  itg2split  25908  itg2monolem1  25909  itg2mono  25912  itg2i1fseqle  25913  itg2i1fseq  25914  itg2addlem  25917  itg2cnlem1  25920  itgeqa  25973  itgfsum  25986  itgabs  25994  itggt0  26003  dvlipcn  26153  dvfsumabs  26182  dvfsumlem2  26186  itgsubstlem  26207  coeeulem  26381  dgrlem  26386  dgrlb  26393  coeaddlem  26406  coecj  26435  coecjOLD  26437  ulmss  26560  leibpi  27107  xrlimcnp  27133  o1cxp  27139  jensen  27153  lgambdd  27201  wilthlem2  27233  sqff1o  27346  fsumdvdscom  27349  fsumdvdsmul  27359  dchrmulcl  27413  dchrmullid  27416  dchrinv  27425  dchrvmasumlem2  27662  ostth1  27797  conway  27972  lesrec  27992  ercgrg  28786  f1otrg  29220  f1otrge  29221  ubthlem2  31223  fmptcof2  33002  disjdsct  33048  fprodex01  33169  prodindf  33182  ccatf1  33269  ressprs  33286  mgcf1o  33323  gsumpart  33383  suppgsumssiun  33392  archiabl  33518  lmodslmd  33524  elrgspnlem1  33562  elrgspnlem2  33563  elrgspnsubrunlem2  33568  rhmimaidl  33740  gsummoncoe1fzo  33887  ply1gsumz  33889  vietadeg1  33968  vietalem  33969  fedgmullem2  34020  fedgmul  34021  txomap  34224  qtophaus  34226  locfinreflem  34230  ordtrest2NEWlem  34312  lmdvg  34343  zrhcntr  34369  esumcl  34420  esumeq2d  34427  esumnul  34438  hasheuni  34475  esumcvg  34476  esumcvgre  34481  insiga  34527  ldsysgenld  34550  ldgenpisyslem1  34553  measvunilem  34602  measvunilem0  34603  measdivcstALTV  34615  cntmeas  34616  voliune  34619  volfiniune  34620  1stmbfm  34650  2ndmbfm  34651  omssubadd  34690  difelcarsg  34700  inelcarsg  34701  eulerpartlems  34750  eulerpartlemsv3  34751  eulerpartlemgvv  34766  dstrvprob  34862  hashreprin  35007  reprgt  35008  breprexplemc  35019  circlemeth  35027  hgt750lema  35044  tgoldbachgtd  35049  bnj93  35251  bnj518  35274  bnj1489  35444  fnrelpredd  35482  subfacp1lem3  35674  subfacp1lem5  35676  erdszelem8  35690  ptpconn  35725  resconn  35738  cvmliftmolem2  35774  cvmlift2lem11  35805  cvmliftphtlem  35809  mclsax  36061  weiunfr  36978  fin2so  38258  poimirlem18  38289  poimirlem21  38292  mblfinlem2  38309  itgabsnc  38340  itggt0cn  38341  prdsbnd  38444  prdstotbnd  38445  prdsbnd2  38446  rrnequiv  38486  eqlkr3  39875  dih1dimatlem  42103  3factsumint  42792  aks6d1c5lem2  42905  fnwe2lem1  43777  cantnf2  44052  nadd1suc  44119  imo72b2  44898  rfcnnnub  45756  disjxp1  45789  disjinfi  45910  fvixp2  45916  dmrelrnrel  45942  fvmptelcdmf  45985  suplesup  46055  infxr  46082  monoord2xrv  46197  climinf  46322  climsuse  46324  mullimc  46332  limccog  46336  mullimcf  46339  limcperiod  46344  limcleqr  46358  neglimc  46361  0ellimcdiv  46363  limclner  46365  limsuppnfdlem  46415  limsupubuzlem  46426  xlimmnfvlem2  46547  xlimpnfvlem2  46551  climxlim2lem  46559  dvdivbd  46637  ioodvbdlimc1lem1  46645  dvnprodlem2  46661  iblsplit  46680  stoweidlem5  46719  stoweidlem16  46730  stoweidlem21  46735  stoweidlem24  46738  stoweidlem25  46739  stoweidlem28  46742  stoweidlem31  46745  stoweidlem41  46755  stoweidlem42  46756  stoweidlem44  46758  stoweidlem45  46759  stoweidlem48  46762  stoweidlem51  46765  stoweidlem54  46768  stoweidlem57  46771  stoweidlem60  46774  stoweidlem62  46776  stirlinglem5  46792  dirkercncflem3  46819  fourierdlem11  46832  fourierdlem12  46833  fourierdlem14  46835  fourierdlem15  46836  fourierdlem31  46852  fourierdlem34  46855  fourierdlem41  46862  fourierdlem48  46868  fourierdlem49  46869  fourierdlem50  46870  fourierdlem54  46874  fourierdlem69  46889  fourierdlem73  46893  fourierdlem74  46894  fourierdlem75  46895  fourierdlem76  46896  fourierdlem79  46899  fourierdlem80  46900  fourierdlem81  46901  fourierdlem92  46912  fourierdlem93  46913  fourierdlem94  46914  fourierdlem97  46917  fourierdlem103  46923  fourierdlem104  46924  fourierdlem111  46931  fourierdlem113  46933  etransclem32  46980  subsaliuncllem  47071  sge0rpcpnf  47135  caragendifcl  47228  iinhoiicclem  47387  pimdecfgtioc  47429  issmfgtlem  47469  ormklocald  47590  ormkglobd  47591  initopropd  50021  termopropd  50022  thincciso2  50233