Theorem r19.21bi 3134

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069

This theorem is referenced by:  r19.21be  3135  rspec2  3136  rspec3  3137  ralxfr2d  5333  fvmptelrn  6987  f1oresrab  6999  isoselem  7212  mpoexw  7919  boxcutc  8729  xpf1o  8926  fineqvlem  9037  indexfi  9127  dffi3  9190  suppr  9230  supiso  9234  infpr  9262  ordtypelem9  9285  brwdom3  9341  xpwdomg  9344  ixpiunwdom  9349  infxpenc2lem1  9775  hsmexlem4  10185  gchina  10455  wunom  10476  prcdnq  10749  prnmax  10751  dedekind  11138  dedekindle  11139  monoord2  13754  limsupgre  15190  limsupbnd1  15191  limsupbnd2  15192  climmpt2  15282  rlimcld2  15287  climsup  15381  sumpr  15460  sumtp  15461  fsum2dlem  15482  fsumiun  15533  fprod2dlem  15690  iserodd  16536  vdwlem1  16682  vdwlem6  16687  vdwnnlem3  16698  imasvscafn  17248  fuciso  17693  evlfcl  17940  yonedainv  17999  acsmapd  18272  prdsmndd  18418  psgnunilem5  19102  gsummpt1n0  19566  dprdspan  19630  ablfaclem2  19689  srgi  19747  srgrz  19762  srglz  19763  issrngd  20121  frgpcyg  20781  psrbaglesupp  21127  psrbaglesuppOLD  21128  psrbagcon  21133  psrbagconOLD  21134  evlslem2  21289  mpfind  21317  gsumsmonply1  21474  gsummoncoe1  21475  evl1gsummon  21531  cpmatmcllem  21867  neiptoptop  22282  neiptopnei  22283  ordtrest2lem  22354  cncmp  22543  1stckgenlem  22704  ptcld  22764  dfac14  22769  ptcnplem  22772  pthaus  22789  xkococnlem  22810  xkococn  22811  cnmpt2k  22839  xpstopnlem1  22960  cnpflfi  23150  ptcmplem2  23204  cnextcn  23218  cnextfres1  23219  cnmpt2plusg  23239  cnmpt2vsca  23346  ustfilxp  23364  utoptop  23386  restutop  23389  restutopopn  23390  ucncn  23437  cfilufg  23445  trcfilu  23446  psmet0  23461  psmettri2  23462  prdsxmetlem  23521  prdsbl  23647  prdsxmslem2  23685  psmetutop  23723  cnmpt2ds  24006  bndth  24121  cnmpt2ip  24412  iscmet3lem2  24456  cmetcusp1  24517  rrxcph  24556  ovoliunlem1  24666  ovoliunlem3  24668  ovoliun  24669  ovoliun2  24670  ovolscalem1  24677  volfiniun  24711  uniioombllem4  24750  mbfeqalem1  24805  mbfres2  24809  ismbf3d  24818  mbfsup  24828  mbfinf  24829  mbflim  24832  itg1ge0  24850  itg1mulc  24869  itg1climres  24879  mbfi1fseqlem4  24883  itg2lea  24909  itg2splitlem  24913  itg2split  24914  itg2monolem1  24915  itg2mono  24918  itg2i1fseqle  24919  itg2i1fseq  24920  itg2addlem  24923  itg2cnlem1  24926  itgeqa  24978  itgfsum  24991  itgabs  24999  itggt0  25008  dvlipcn  25158  dvfsumabs  25187  dvfsumlem2  25191  itgsubstlem  25212  coeeulem  25385  dgrlem  25390  dgrlb  25397  coeaddlem  25410  coecj  25439  ulmss  25556  leibpi  26092  xrlimcnp  26118  o1cxp  26124  jensen  26138  lgambdd  26186  wilthlem2  26218  sqff1o  26331  fsumdvdscom  26334  fsumdvdsmul  26344  dchrmulcl  26397  dchrmulid2  26400  dchrinv  26409  dchrvmasumlem2  26646  ostth1  26781  ercgrg  26878  f1otrg  27232  f1otrge  27233  ubthlem2  29233  fmptcof2  30994  disjdsct  31035  fprodex01  31139  ccatf1  31223  ressprs  31241  oduprs  31242  mgcf1o  31281  gsumpart  31315  archiabl  31452  lmodslmd  31457  rhmimaidl  31609  ply1chr  31669  fedgmullem2  31711  fedgmul  31712  txomap  31784  qtophaus  31786  locfinreflem  31790  ordtrest2NEWlem  31872  lmdvg  31903  prodindf  31991  esumcl  31998  esumeq2d  32005  esumnul  32016  hasheuni  32053  esumcvg  32054  esumcvgre  32059  insiga  32105  ldsysgenld  32128  ldgenpisyslem1  32131  measvunilem  32180  measvunilem0  32181  measdivcstALTV  32193  cntmeas  32194  voliune  32197  volfiniune  32198  1stmbfm  32227  2ndmbfm  32228  omssubadd  32267  difelcarsg  32277  inelcarsg  32278  eulerpartlems  32327  eulerpartlemsv3  32328  eulerpartlemgvv  32343  dstrvprob  32438  hashreprin  32600  reprgt  32601  breprexplemc  32612  circlemeth  32620  hgt750lema  32637  tgoldbachgtd  32642  bnj93  32843  bnj518  32866  bnj1489  33036  fnrelpredd  33061  subfacp1lem3  33144  subfacp1lem5  33146  erdszelem8  33160  ptpconn  33195  resconn  33208  cvmliftmolem2  33244  cvmlift2lem11  33275  cvmliftphtlem  33279  mclsax  33531  conway  33993  slerec  34013  fin2so  35764  poimirlem18  35795  poimirlem21  35798  mblfinlem2  35815  itgabsnc  35846  itggt0cn  35847  prdsbnd  35951  prdstotbnd  35952  prdsbnd2  35953  rrnequiv  35993  eqlkr3  37115  dih1dimatlem  39343  3factsumint  40033  fnwe2lem1  40875  imo72b2  41783  rfcnnnub  42579  disjxp1  42617  fompt  42730  disjinfi  42731  fvixp2  42738  dmrelrnrel  42765  suplesup  42878  infxr  42906  monoord2xrv  43024  climinf  43147  climsuse  43149  mullimc  43157  limccog  43161  mullimcf  43164  limcperiod  43169  limcleqr  43185  neglimc  43188  0ellimcdiv  43190  limclner  43192  limsuppnfdlem  43242  limsupubuzlem  43253  xlimmnfvlem2  43374  xlimpnfvlem2  43378  climxlim2lem  43386  dvdivbd  43464  ioodvbdlimc1lem1  43472  dvnprodlem2  43488  iblsplit  43507  stoweidlem5  43546  stoweidlem16  43557  stoweidlem21  43562  stoweidlem24  43565  stoweidlem25  43566  stoweidlem28  43569  stoweidlem31  43572  stoweidlem41  43582  stoweidlem42  43583  stoweidlem44  43585  stoweidlem45  43586  stoweidlem48  43589  stoweidlem51  43592  stoweidlem54  43595  stoweidlem57  43598  stoweidlem60  43601  stoweidlem62  43603  stirlinglem5  43619  dirkercncflem3  43646  fourierdlem11  43659  fourierdlem12  43660  fourierdlem14  43662  fourierdlem15  43663  fourierdlem31  43679  fourierdlem34  43682  fourierdlem41  43689  fourierdlem48  43695  fourierdlem49  43696  fourierdlem50  43697  fourierdlem54  43701  fourierdlem69  43716  fourierdlem73  43720  fourierdlem74  43721  fourierdlem75  43722  fourierdlem76  43723  fourierdlem79  43726  fourierdlem80  43727  fourierdlem81  43728  fourierdlem92  43739  fourierdlem93  43740  fourierdlem94  43741  fourierdlem97  43744  fourierdlem103  43750  fourierdlem104  43751  fourierdlem111  43758  fourierdlem113  43760  etransclem32  43807  subsaliuncllem  43896  sge0rpcpnf  43959  caragendifcl  44052  iinhoiicclem  44211  pimdecfgtioc  44252  issmfgtlem  44291