Theorem r19.21bi 3229

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045

This theorem is referenced by:  r19.21be  3230  rspec2  3256  rspec3  3257  ralxfr2d  5365  fvmptelcdm  7085  fompt  7090  f1oresrab  7099  isoselem  7316  mpoexw  8057  naddsuc2  8665  boxcutc  8914  xpf1o  9103  fineqvlem  9209  indexfi  9311  dffi3  9382  suppr  9423  supiso  9427  infpr  9456  ordtypelem9  9479  brwdom3  9535  xpwdomg  9538  ixpiunwdom  9543  infxpenc2lem1  9972  hsmexlem4  10382  gchina  10652  wunom  10673  prcdnq  10946  prnmax  10948  dedekind  11337  dedekindle  11338  monoord2  13998  limsupgre  15447  limsupbnd1  15448  limsupbnd2  15449  climmpt2  15539  rlimcld2  15544  climsup  15636  sumpr  15714  sumtp  15715  fsum2dlem  15736  fsumiun  15787  fprod2dlem  15946  iserodd  16806  vdwlem1  16952  vdwlem6  16957  vdwnnlem3  16968  imasvscafn  17500  fuciso  17940  evlfcl  18183  yonedainv  18242  oduprs  18261  acsmapd  18513  prdsmndd  18697  psgnunilem5  19424  gsummpt1n0  19895  dprdspan  19959  ablfaclem2  20018  srgdilem  20101  srgrz  20116  srglz  20117  issrngd  20764  frgpcyg  21483  psrbaglesupp  21831  psrbagcon  21834  psrbagleadd1  21837  evlslem2  21986  mpfind  22014  psdmul  22053  ply1chr  22193  gsumsmonply1  22194  gsummoncoe1  22195  evl1gsummon  22252  cpmatmcllem  22605  neiptoptop  23018  neiptopnei  23019  ordtrest2lem  23090  cncmp  23279  1stckgenlem  23440  ptcld  23500  dfac14  23505  ptcnplem  23508  pthaus  23525  xkococnlem  23546  xkococn  23547  cnmpt2k  23575  xpstopnlem1  23696  cnpflfi  23886  ptcmplem2  23940  cnextcn  23954  cnextfres1  23955  cnmpt2plusg  23975  cnmpt2vsca  24082  ustfilxp  24100  utoptop  24122  restutop  24125  restutopopn  24126  ucncn  24172  cfilufg  24180  trcfilu  24181  psmet0  24196  psmettri2  24197  prdsxmetlem  24256  prdsbl  24379  prdsxmslem2  24417  psmetutop  24455  cnmpt2ds  24732  bndth  24857  cnmpt2ip  25148  iscmet3lem2  25192  cmetcusp1  25253  rrxcph  25292  ovoliunlem1  25403  ovoliunlem3  25405  ovoliun  25406  ovoliun2  25407  ovolscalem1  25414  volfiniun  25448  uniioombllem4  25487  mbfeqalem1  25542  mbfres2  25546  ismbf3d  25555  mbfsup  25565  mbfinf  25566  mbflim  25569  itg1ge0  25587  itg1mulc  25605  itg1climres  25615  mbfi1fseqlem4  25619  itg2lea  25645  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2mono  25654  itg2i1fseqle  25655  itg2i1fseq  25656  itg2addlem  25659  itg2cnlem1  25662  itgeqa  25715  itgfsum  25728  itgabs  25736  itggt0  25745  dvlipcn  25899  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  itgsubstlem  25955  coeeulem  26129  dgrlem  26134  dgrlb  26141  coeaddlem  26154  coecj  26184  coecjOLD  26186  ulmss  26306  leibpi  26852  xrlimcnp  26878  o1cxp  26885  jensen  26899  lgambdd  26947  wilthlem2  26979  sqff1o  27092  fsumdvdscom  27095  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  dchrmulcl  27160  dchrmullid  27163  dchrinv  27172  dchrvmasumlem2  27409  ostth1  27544  conway  27711  slerec  27731  ercgrg  28444  f1otrg  28798  f1otrge  28799  ubthlem2  30800  fmptcof2  32581  disjdsct  32626  fprodex01  32750  prodindf  32786  ccatf1  32870  ressprs  32890  mgcf1o  32929  chnccats1  32941  gsumpart  32997  archiabl  33152  lmodslmd  33157  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnsubrunlem2  33199  rhmimaidl  33403  gsummoncoe1fzo  33563  ply1gsumz  33564  fedgmullem2  33626  fedgmul  33627  txomap  33824  qtophaus  33826  locfinreflem  33830  ordtrest2NEWlem  33912  lmdvg  33943  zrhcntr  33969  esumcl  34020  esumeq2d  34027  esumnul  34038  hasheuni  34075  esumcvg  34076  esumcvgre  34081  insiga  34127  ldsysgenld  34150  ldgenpisyslem1  34153  measvunilem  34202  measvunilem0  34203  measdivcstALTV  34215  cntmeas  34216  voliune  34219  volfiniune  34220  1stmbfm  34251  2ndmbfm  34252  omssubadd  34291  difelcarsg  34301  inelcarsg  34302  eulerpartlems  34351  eulerpartlemsv3  34352  eulerpartlemgvv  34367  dstrvprob  34463  hashreprin  34611  reprgt  34612  breprexplemc  34623  circlemeth  34631  hgt750lema  34648  tgoldbachgtd  34653  bnj93  34853  bnj518  34876  bnj1489  35046  fnrelpredd  35079  subfacp1lem3  35169  subfacp1lem5  35171  erdszelem8  35185  ptpconn  35220  resconn  35233  cvmliftmolem2  35269  cvmlift2lem11  35300  cvmliftphtlem  35304  mclsax  35556  weiunfr  36455  fin2so  37601  poimirlem18  37632  poimirlem21  37635  mblfinlem2  37652  itgabsnc  37683  itggt0cn  37684  prdsbnd  37787  prdstotbnd  37788  prdsbnd2  37789  rrnequiv  37829  eqlkr3  39094  dih1dimatlem  41323  3factsumint  42013  aks6d1c5lem2  42126  fnwe2lem1  43039  cantnf2  43314  nadd1suc  43381  imo72b2  44161  rfcnnnub  45030  disjxp1  45063  disjinfi  45186  fvixp2  45193  dmrelrnrel  45220  fvmptelcdmf  45264  suplesup  45335  infxr  45363  monoord2xrv  45479  climinf  45604  climsuse  45606  mullimc  45614  limccog  45618  mullimcf  45621  limcperiod  45626  limcleqr  45642  neglimc  45645  0ellimcdiv  45647  limclner  45649  limsuppnfdlem  45699  limsupubuzlem  45710  xlimmnfvlem2  45831  xlimpnfvlem2  45835  climxlim2lem  45843  dvdivbd  45921  ioodvbdlimc1lem1  45929  dvnprodlem2  45945  iblsplit  45964  stoweidlem5  46003  stoweidlem16  46014  stoweidlem21  46019  stoweidlem24  46022  stoweidlem25  46023  stoweidlem28  46026  stoweidlem31  46029  stoweidlem41  46039  stoweidlem42  46040  stoweidlem44  46042  stoweidlem45  46043  stoweidlem48  46046  stoweidlem51  46049  stoweidlem54  46052  stoweidlem57  46055  stoweidlem60  46058  stoweidlem62  46060  stirlinglem5  46076  dirkercncflem3  46103  fourierdlem11  46116  fourierdlem12  46117  fourierdlem14  46119  fourierdlem15  46120  fourierdlem31  46136  fourierdlem34  46139  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem54  46158  fourierdlem69  46173  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem79  46183  fourierdlem80  46184  fourierdlem81  46185  fourierdlem92  46196  fourierdlem93  46197  fourierdlem94  46198  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem113  46217  etransclem32  46264  subsaliuncllem  46355  sge0rpcpnf  46419  caragendifcl  46512  iinhoiicclem  46671  pimdecfgtioc  46713  issmfgtlem  46753  ormklocald  46872  ormkglobd  46873  initopropd  49232  termopropd  49233  thincciso2  49444