Theorem r19.21bi 3230

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

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

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 3046

This theorem is referenced by:  r19.21be  3231  rspec2  3257  rspec3  3258  ralxfr2d  5368  fvmptelcdm  7088  fompt  7093  f1oresrab  7102  isoselem  7319  mpoexw  8060  naddsuc2  8668  boxcutc  8917  xpf1o  9109  fineqvlem  9216  indexfi  9318  dffi3  9389  suppr  9430  supiso  9434  infpr  9463  ordtypelem9  9486  brwdom3  9542  xpwdomg  9545  ixpiunwdom  9550  infxpenc2lem1  9979  hsmexlem4  10389  gchina  10659  wunom  10680  prcdnq  10953  prnmax  10955  dedekind  11344  dedekindle  11345  monoord2  14005  limsupgre  15454  limsupbnd1  15455  limsupbnd2  15456  climmpt2  15546  rlimcld2  15551  climsup  15643  sumpr  15721  sumtp  15722  fsum2dlem  15743  fsumiun  15794  fprod2dlem  15953  iserodd  16813  vdwlem1  16959  vdwlem6  16964  vdwnnlem3  16975  imasvscafn  17507  fuciso  17947  evlfcl  18190  yonedainv  18249  oduprs  18268  acsmapd  18520  prdsmndd  18704  psgnunilem5  19431  gsummpt1n0  19902  dprdspan  19966  ablfaclem2  20025  srgdilem  20108  srgrz  20123  srglz  20124  issrngd  20771  frgpcyg  21490  psrbaglesupp  21838  psrbagcon  21841  psrbagleadd1  21844  evlslem2  21993  mpfind  22021  psdmul  22060  ply1chr  22200  gsumsmonply1  22201  gsummoncoe1  22202  evl1gsummon  22259  cpmatmcllem  22612  neiptoptop  23025  neiptopnei  23026  ordtrest2lem  23097  cncmp  23286  1stckgenlem  23447  ptcld  23507  dfac14  23512  ptcnplem  23515  pthaus  23532  xkococnlem  23553  xkococn  23554  cnmpt2k  23582  xpstopnlem1  23703  cnpflfi  23893  ptcmplem2  23947  cnextcn  23961  cnextfres1  23962  cnmpt2plusg  23982  cnmpt2vsca  24089  ustfilxp  24107  utoptop  24129  restutop  24132  restutopopn  24133  ucncn  24179  cfilufg  24187  trcfilu  24188  psmet0  24203  psmettri2  24204  prdsxmetlem  24263  prdsbl  24386  prdsxmslem2  24424  psmetutop  24462  cnmpt2ds  24739  bndth  24864  cnmpt2ip  25155  iscmet3lem2  25199  cmetcusp1  25260  rrxcph  25299  ovoliunlem1  25410  ovoliunlem3  25412  ovoliun  25413  ovoliun2  25414  ovolscalem1  25421  volfiniun  25455  uniioombllem4  25494  mbfeqalem1  25549  mbfres2  25553  ismbf3d  25562  mbfsup  25572  mbfinf  25573  mbflim  25576  itg1ge0  25594  itg1mulc  25612  itg1climres  25622  mbfi1fseqlem4  25626  itg2lea  25652  itg2splitlem  25656  itg2split  25657  itg2monolem1  25658  itg2mono  25661  itg2i1fseqle  25662  itg2i1fseq  25663  itg2addlem  25666  itg2cnlem1  25669  itgeqa  25722  itgfsum  25735  itgabs  25743  itggt0  25752  dvlipcn  25906  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  itgsubstlem  25962  coeeulem  26136  dgrlem  26141  dgrlb  26148  coeaddlem  26161  coecj  26191  coecjOLD  26193  ulmss  26313  leibpi  26859  xrlimcnp  26885  o1cxp  26892  jensen  26906  lgambdd  26954  wilthlem2  26986  sqff1o  27099  fsumdvdscom  27102  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  dchrmulcl  27167  dchrmullid  27170  dchrinv  27179  dchrvmasumlem2  27416  ostth1  27551  conway  27718  slerec  27738  ercgrg  28451  f1otrg  28805  f1otrge  28806  ubthlem2  30807  fmptcof2  32588  disjdsct  32633  fprodex01  32757  prodindf  32793  ccatf1  32877  ressprs  32897  mgcf1o  32936  chnccats1  32948  gsumpart  33004  archiabl  33159  lmodslmd  33164  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnsubrunlem2  33206  rhmimaidl  33410  gsummoncoe1fzo  33570  ply1gsumz  33571  fedgmullem2  33633  fedgmul  33634  txomap  33831  qtophaus  33833  locfinreflem  33837  ordtrest2NEWlem  33919  lmdvg  33950  zrhcntr  33976  esumcl  34027  esumeq2d  34034  esumnul  34045  hasheuni  34082  esumcvg  34083  esumcvgre  34088  insiga  34134  ldsysgenld  34157  ldgenpisyslem1  34160  measvunilem  34209  measvunilem0  34210  measdivcstALTV  34222  cntmeas  34223  voliune  34226  volfiniune  34227  1stmbfm  34258  2ndmbfm  34259  omssubadd  34298  difelcarsg  34308  inelcarsg  34309  eulerpartlems  34358  eulerpartlemsv3  34359  eulerpartlemgvv  34374  dstrvprob  34470  hashreprin  34618  reprgt  34619  breprexplemc  34630  circlemeth  34638  hgt750lema  34655  tgoldbachgtd  34660  bnj93  34860  bnj518  34883  bnj1489  35053  fnrelpredd  35086  subfacp1lem3  35176  subfacp1lem5  35178  erdszelem8  35192  ptpconn  35227  resconn  35240  cvmliftmolem2  35276  cvmlift2lem11  35307  cvmliftphtlem  35311  mclsax  35563  weiunfr  36462  fin2so  37608  poimirlem18  37639  poimirlem21  37642  mblfinlem2  37659  itgabsnc  37690  itggt0cn  37691  prdsbnd  37794  prdstotbnd  37795  prdsbnd2  37796  rrnequiv  37836  eqlkr3  39101  dih1dimatlem  41330  3factsumint  42020  aks6d1c5lem2  42133  fnwe2lem1  43046  cantnf2  43321  nadd1suc  43388  imo72b2  44168  rfcnnnub  45037  disjxp1  45070  disjinfi  45193  fvixp2  45200  dmrelrnrel  45227  fvmptelcdmf  45271  suplesup  45342  infxr  45370  monoord2xrv  45486  climinf  45611  climsuse  45613  mullimc  45621  limccog  45625  mullimcf  45628  limcperiod  45633  limcleqr  45649  neglimc  45652  0ellimcdiv  45654  limclner  45656  limsuppnfdlem  45706  limsupubuzlem  45717  xlimmnfvlem2  45838  xlimpnfvlem2  45842  climxlim2lem  45850  dvdivbd  45928  ioodvbdlimc1lem1  45936  dvnprodlem2  45952  iblsplit  45971  stoweidlem5  46010  stoweidlem16  46021  stoweidlem21  46026  stoweidlem24  46029  stoweidlem25  46030  stoweidlem28  46033  stoweidlem31  46036  stoweidlem41  46046  stoweidlem42  46047  stoweidlem44  46049  stoweidlem45  46050  stoweidlem48  46053  stoweidlem51  46056  stoweidlem54  46059  stoweidlem57  46062  stoweidlem60  46065  stoweidlem62  46067  stirlinglem5  46083  dirkercncflem3  46110  fourierdlem11  46123  fourierdlem12  46124  fourierdlem14  46126  fourierdlem15  46127  fourierdlem31  46143  fourierdlem34  46146  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem54  46165  fourierdlem69  46180  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem79  46190  fourierdlem80  46191  fourierdlem81  46192  fourierdlem92  46203  fourierdlem93  46204  fourierdlem94  46205  fourierdlem97  46208  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem113  46224  etransclem32  46271  subsaliuncllem  46362  sge0rpcpnf  46426  caragendifcl  46519  iinhoiicclem  46678  pimdecfgtioc  46720  issmfgtlem  46760  ormklocald  46879  ormkglobd  46880  initopropd  49236  termopropd  49237  thincciso2  49448