Theorem r19.21bi 3248

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-ral 3059

This theorem is referenced by:  r19.21be  3249  rspec2  3276  rspec3  3277  ralxfr2d  5415  fvmptelcdm  7132  fompt  7137  f1oresrab  7146  isoselem  7360  mpoexw  8101  naddsuc2  8737  boxcutc  8979  xpf1o  9177  fineqvlem  9295  indexfi  9397  dffi3  9468  suppr  9508  supiso  9512  infpr  9540  ordtypelem9  9563  brwdom3  9619  xpwdomg  9622  ixpiunwdom  9627  infxpenc2lem1  10056  hsmexlem4  10466  gchina  10736  wunom  10757  prcdnq  11030  prnmax  11032  dedekind  11421  dedekindle  11422  monoord2  14070  limsupgre  15513  limsupbnd1  15514  limsupbnd2  15515  climmpt2  15605  rlimcld2  15610  climsup  15702  sumpr  15780  sumtp  15781  fsum2dlem  15802  fsumiun  15853  fprod2dlem  16012  iserodd  16868  vdwlem1  17014  vdwlem6  17019  vdwnnlem3  17030  imasvscafn  17583  fuciso  18031  evlfcl  18278  yonedainv  18337  oduprs  18357  acsmapd  18611  prdsmndd  18795  psgnunilem5  19526  gsummpt1n0  19997  dprdspan  20061  ablfaclem2  20120  srgdilem  20209  srgrz  20224  srglz  20225  issrngd  20872  frgpcyg  21609  psrbaglesupp  21959  psrbagcon  21962  psrbagleadd1  21965  evlslem2  22120  mpfind  22148  psdmul  22187  ply1chr  22325  gsumsmonply1  22326  gsummoncoe1  22327  evl1gsummon  22384  cpmatmcllem  22739  neiptoptop  23154  neiptopnei  23155  ordtrest2lem  23226  cncmp  23415  1stckgenlem  23576  ptcld  23636  dfac14  23641  ptcnplem  23644  pthaus  23661  xkococnlem  23682  xkococn  23683  cnmpt2k  23711  xpstopnlem1  23832  cnpflfi  24022  ptcmplem2  24076  cnextcn  24090  cnextfres1  24091  cnmpt2plusg  24111  cnmpt2vsca  24218  ustfilxp  24236  utoptop  24258  restutop  24261  restutopopn  24262  ucncn  24309  cfilufg  24317  trcfilu  24318  psmet0  24333  psmettri2  24334  prdsxmetlem  24393  prdsbl  24519  prdsxmslem2  24557  psmetutop  24595  cnmpt2ds  24878  bndth  25003  cnmpt2ip  25295  iscmet3lem2  25339  cmetcusp1  25400  rrxcph  25439  ovoliunlem1  25550  ovoliunlem3  25552  ovoliun  25553  ovoliun2  25554  ovolscalem1  25561  volfiniun  25595  uniioombllem4  25634  mbfeqalem1  25689  mbfres2  25693  ismbf3d  25702  mbfsup  25712  mbfinf  25713  mbflim  25716  itg1ge0  25734  itg1mulc  25753  itg1climres  25763  mbfi1fseqlem4  25767  itg2lea  25793  itg2splitlem  25797  itg2split  25798  itg2monolem1  25799  itg2mono  25802  itg2i1fseqle  25803  itg2i1fseq  25804  itg2addlem  25807  itg2cnlem1  25810  itgeqa  25863  itgfsum  25876  itgabs  25884  itggt0  25893  dvlipcn  26047  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  itgsubstlem  26103  coeeulem  26277  dgrlem  26282  dgrlb  26289  coeaddlem  26302  coecj  26332  coecjOLD  26334  ulmss  26454  leibpi  26999  xrlimcnp  27025  o1cxp  27032  jensen  27046  lgambdd  27094  wilthlem2  27126  sqff1o  27239  fsumdvdscom  27242  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  dchrmulcl  27307  dchrmullid  27310  dchrinv  27319  dchrvmasumlem2  27556  ostth1  27691  conway  27858  slerec  27878  ercgrg  28539  f1otrg  28893  f1otrge  28894  ubthlem2  30899  fmptcof2  32673  disjdsct  32717  fprodex01  32831  ccatf1  32917  ressprs  32938  mgcf1o  32977  gsumpart  33042  archiabl  33187  lmodslmd  33192  elrgspnlem1  33231  elrgspnlem2  33232  rhmimaidl  33439  gsummoncoe1fzo  33597  ply1gsumz  33598  fedgmullem2  33657  fedgmul  33658  txomap  33794  qtophaus  33796  locfinreflem  33800  ordtrest2NEWlem  33882  lmdvg  33913  zrhcntr  33941  prodindf  34003  esumcl  34010  esumeq2d  34017  esumnul  34028  hasheuni  34065  esumcvg  34066  esumcvgre  34071  insiga  34117  ldsysgenld  34140  ldgenpisyslem1  34143  measvunilem  34192  measvunilem0  34193  measdivcstALTV  34205  cntmeas  34206  voliune  34209  volfiniune  34210  1stmbfm  34241  2ndmbfm  34242  omssubadd  34281  difelcarsg  34291  inelcarsg  34292  eulerpartlems  34341  eulerpartlemsv3  34342  eulerpartlemgvv  34357  dstrvprob  34452  hashreprin  34613  reprgt  34614  breprexplemc  34625  circlemeth  34633  hgt750lema  34650  tgoldbachgtd  34655  bnj93  34855  bnj518  34878  bnj1489  35048  fnrelpredd  35081  subfacp1lem3  35166  subfacp1lem5  35168  erdszelem8  35182  ptpconn  35217  resconn  35230  cvmliftmolem2  35266  cvmlift2lem11  35297  cvmliftphtlem  35301  mclsax  35553  weiunfr  36449  fin2so  37593  poimirlem18  37624  poimirlem21  37627  mblfinlem2  37644  itgabsnc  37675  itggt0cn  37676  prdsbnd  37779  prdstotbnd  37780  prdsbnd2  37781  rrnequiv  37821  eqlkr3  39082  dih1dimatlem  41311  3factsumint  42006  aks6d1c5lem2  42119  fnwe2lem1  43038  cantnf2  43314  nadd1suc  43381  imo72b2  44161  rfcnnnub  44973  disjxp1  45008  disjinfi  45134  fvixp2  45141  dmrelrnrel  45168  fvmptelcdmf  45215  suplesup  45288  infxr  45316  monoord2xrv  45433  climinf  45561  climsuse  45563  mullimc  45571  limccog  45575  mullimcf  45578  limcperiod  45583  limcleqr  45599  neglimc  45602  0ellimcdiv  45604  limclner  45606  limsuppnfdlem  45656  limsupubuzlem  45667  xlimmnfvlem2  45788  xlimpnfvlem2  45792  climxlim2lem  45800  dvdivbd  45878  ioodvbdlimc1lem1  45886  dvnprodlem2  45902  iblsplit  45921  stoweidlem5  45960  stoweidlem16  45971  stoweidlem21  45976  stoweidlem24  45979  stoweidlem25  45980  stoweidlem28  45983  stoweidlem31  45986  stoweidlem41  45996  stoweidlem42  45997  stoweidlem44  45999  stoweidlem45  46000  stoweidlem48  46003  stoweidlem51  46006  stoweidlem54  46009  stoweidlem57  46012  stoweidlem60  46015  stoweidlem62  46017  stirlinglem5  46033  dirkercncflem3  46060  fourierdlem11  46073  fourierdlem12  46074  fourierdlem14  46076  fourierdlem15  46077  fourierdlem31  46093  fourierdlem34  46096  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem54  46115  fourierdlem69  46130  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem79  46140  fourierdlem80  46141  fourierdlem81  46142  fourierdlem92  46153  fourierdlem93  46154  fourierdlem94  46155  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem113  46174  etransclem32  46221  subsaliuncllem  46312  sge0rpcpnf  46376  caragendifcl  46469  iinhoiicclem  46628  pimdecfgtioc  46670  issmfgtlem  46710