Theorem r19.21bi 3132

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068

This theorem is referenced by:  r19.21be  3133  rspec2  3134  rspec3  3135  ralxfr2d  5328  fvmptelrn  6969  f1oresrab  6981  isoselem  7192  mpoexw  7892  boxcutc  8687  xpf1o  8875  fineqvlem  8966  indexfi  9057  dffi3  9120  suppr  9160  supiso  9164  infpr  9192  ordtypelem9  9215  brwdom3  9271  xpwdomg  9274  ixpiunwdom  9279  infxpenc2lem1  9706  hsmexlem4  10116  gchina  10386  wunom  10407  prcdnq  10680  prnmax  10682  dedekind  11068  dedekindle  11069  monoord2  13682  limsupgre  15118  limsupbnd1  15119  limsupbnd2  15120  climmpt2  15210  rlimcld2  15215  climsup  15309  sumpr  15388  sumtp  15389  fsum2dlem  15410  fsumiun  15461  fprod2dlem  15618  iserodd  16464  vdwlem1  16610  vdwlem6  16615  vdwnnlem3  16626  imasvscafn  17165  fuciso  17609  evlfcl  17856  yonedainv  17915  acsmapd  18187  prdsmndd  18333  psgnunilem5  19017  gsummpt1n0  19481  dprdspan  19545  ablfaclem2  19604  srgi  19662  srgrz  19677  srglz  19678  issrngd  20036  frgpcyg  20693  psrbaglesupp  21037  psrbaglesuppOLD  21038  psrbagcon  21043  psrbagconOLD  21044  evlslem2  21199  mpfind  21227  gsumsmonply1  21384  gsummoncoe1  21385  evl1gsummon  21441  cpmatmcllem  21775  neiptoptop  22190  neiptopnei  22191  ordtrest2lem  22262  cncmp  22451  1stckgenlem  22612  ptcld  22672  dfac14  22677  ptcnplem  22680  pthaus  22697  xkococnlem  22718  xkococn  22719  cnmpt2k  22747  xpstopnlem1  22868  cnpflfi  23058  ptcmplem2  23112  cnextcn  23126  cnextfres1  23127  cnmpt2plusg  23147  cnmpt2vsca  23254  ustfilxp  23272  utoptop  23294  restutop  23297  restutopopn  23298  ucncn  23345  cfilufg  23353  trcfilu  23354  psmet0  23369  psmettri2  23370  prdsxmetlem  23429  prdsbl  23553  prdsxmslem2  23591  psmetutop  23629  cnmpt2ds  23912  bndth  24027  cnmpt2ip  24317  iscmet3lem2  24361  cmetcusp1  24422  rrxcph  24461  ovoliunlem1  24571  ovoliunlem3  24573  ovoliun  24574  ovoliun2  24575  ovolscalem1  24582  volfiniun  24616  uniioombllem4  24655  mbfeqalem1  24710  mbfres2  24714  ismbf3d  24723  mbfsup  24733  mbfinf  24734  mbflim  24737  itg1ge0  24755  itg1mulc  24774  itg1climres  24784  mbfi1fseqlem4  24788  itg2lea  24814  itg2splitlem  24818  itg2split  24819  itg2monolem1  24820  itg2mono  24823  itg2i1fseqle  24824  itg2i1fseq  24825  itg2addlem  24828  itg2cnlem1  24831  itgeqa  24883  itgfsum  24896  itgabs  24904  itggt0  24913  dvlipcn  25063  dvfsumabs  25092  dvfsumlem2  25096  itgsubstlem  25117  coeeulem  25290  dgrlem  25295  dgrlb  25302  coeaddlem  25315  coecj  25344  ulmss  25461  leibpi  25997  xrlimcnp  26023  o1cxp  26029  jensen  26043  lgambdd  26091  wilthlem2  26123  sqff1o  26236  fsumdvdscom  26239  fsumdvdsmul  26249  dchrmulcl  26302  dchrmulid2  26305  dchrinv  26314  dchrvmasumlem2  26551  ostth1  26686  ercgrg  26782  f1otrg  27136  f1otrge  27137  ubthlem2  29134  fmptcof2  30896  disjdsct  30937  fprodex01  31041  ccatf1  31125  ressprs  31143  oduprs  31144  mgcf1o  31183  gsumpart  31217  archiabl  31354  lmodslmd  31359  rhmimaidl  31511  ply1chr  31571  fedgmullem2  31613  fedgmul  31614  txomap  31686  qtophaus  31688  locfinreflem  31692  ordtrest2NEWlem  31774  lmdvg  31805  prodindf  31891  esumcl  31898  esumeq2d  31905  esumnul  31916  hasheuni  31953  esumcvg  31954  esumcvgre  31959  insiga  32005  ldsysgenld  32028  ldgenpisyslem1  32031  measvunilem  32080  measvunilem0  32081  measdivcstALTV  32093  cntmeas  32094  voliune  32097  volfiniune  32098  1stmbfm  32127  2ndmbfm  32128  omssubadd  32167  difelcarsg  32177  inelcarsg  32178  eulerpartlems  32227  eulerpartlemsv3  32228  eulerpartlemgvv  32243  dstrvprob  32338  hashreprin  32500  reprgt  32501  breprexplemc  32512  circlemeth  32520  hgt750lema  32537  tgoldbachgtd  32542  bnj93  32743  bnj518  32766  bnj1489  32936  fnrelpredd  32961  subfacp1lem3  33044  subfacp1lem5  33046  erdszelem8  33060  ptpconn  33095  resconn  33108  cvmliftmolem2  33144  cvmlift2lem11  33175  cvmliftphtlem  33179  mclsax  33431  conway  33920  slerec  33940  fin2so  35691  poimirlem18  35722  poimirlem21  35725  mblfinlem2  35742  itgabsnc  35773  itggt0cn  35774  prdsbnd  35878  prdstotbnd  35879  prdsbnd2  35880  rrnequiv  35920  eqlkr3  37042  dih1dimatlem  39270  3factsumint  39961  fnwe2lem1  40791  imo72b2  41672  rfcnnnub  42468  disjxp1  42506  fompt  42619  disjinfi  42620  fvixp2  42627  dmrelrnrel  42654  suplesup  42768  infxr  42796  monoord2xrv  42914  climinf  43037  climsuse  43039  mullimc  43047  limccog  43051  mullimcf  43054  limcperiod  43059  limcleqr  43075  neglimc  43078  0ellimcdiv  43080  limclner  43082  limsuppnfdlem  43132  limsupubuzlem  43143  xlimmnfvlem2  43264  xlimpnfvlem2  43268  climxlim2lem  43276  dvdivbd  43354  ioodvbdlimc1lem1  43362  dvnprodlem2  43378  iblsplit  43397  stoweidlem5  43436  stoweidlem16  43447  stoweidlem21  43452  stoweidlem24  43455  stoweidlem25  43456  stoweidlem28  43459  stoweidlem31  43462  stoweidlem41  43472  stoweidlem42  43473  stoweidlem44  43475  stoweidlem45  43476  stoweidlem48  43479  stoweidlem51  43482  stoweidlem54  43485  stoweidlem57  43488  stoweidlem60  43491  stoweidlem62  43493  stirlinglem5  43509  dirkercncflem3  43536  fourierdlem11  43549  fourierdlem12  43550  fourierdlem14  43552  fourierdlem15  43553  fourierdlem31  43569  fourierdlem34  43572  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem54  43591  fourierdlem69  43606  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem79  43616  fourierdlem80  43617  fourierdlem81  43618  fourierdlem92  43629  fourierdlem93  43630  fourierdlem94  43631  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem113  43650  etransclem32  43697  subsaliuncllem  43786  sge0rpcpnf  43849  caragendifcl  43942  iinhoiicclem  44101  pimdecfgtioc  44139  issmfgtlem  44178