Theorem r19.21bi 3221

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 3218	. 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  3222  rspec2  3248  rspec3  3249  ralxfr2d  5349  fvmptelcdm  7047  fompt  7052  f1oresrab  7061  isoselem  7278  mpoexw  8013  naddsuc2  8619  boxcutc  8868  xpf1o  9056  fineqvlem  9155  indexfi  9250  dffi3  9321  suppr  9362  supiso  9366  infpr  9395  ordtypelem9  9418  brwdom3  9474  xpwdomg  9477  ixpiunwdom  9482  infxpenc2lem1  9913  hsmexlem4  10323  gchina  10593  wunom  10614  prcdnq  10887  prnmax  10889  dedekind  11279  dedekindle  11280  monoord2  13940  limsupgre  15388  limsupbnd1  15389  limsupbnd2  15390  climmpt2  15480  rlimcld2  15485  climsup  15577  sumpr  15655  sumtp  15656  fsum2dlem  15677  fsumiun  15728  fprod2dlem  15887  iserodd  16747  vdwlem1  16893  vdwlem6  16898  vdwnnlem3  16909  imasvscafn  17441  fuciso  17885  evlfcl  18128  yonedainv  18187  oduprs  18206  acsmapd  18460  prdsmndd  18644  psgnunilem5  19373  gsummpt1n0  19844  dprdspan  19908  ablfaclem2  19967  srgdilem  20077  srgrz  20092  srglz  20093  issrngd  20740  frgpcyg  21480  psrbaglesupp  21829  psrbagcon  21832  psrbagleadd1  21835  evlslem2  21984  mpfind  22012  psdmul  22051  ply1chr  22191  gsumsmonply1  22192  gsummoncoe1  22193  evl1gsummon  22250  cpmatmcllem  22603  neiptoptop  23016  neiptopnei  23017  ordtrest2lem  23088  cncmp  23277  1stckgenlem  23438  ptcld  23498  dfac14  23503  ptcnplem  23506  pthaus  23523  xkococnlem  23544  xkococn  23545  cnmpt2k  23573  xpstopnlem1  23694  cnpflfi  23884  ptcmplem2  23938  cnextcn  23952  cnextfres1  23953  cnmpt2plusg  23973  cnmpt2vsca  24080  ustfilxp  24098  utoptop  24120  restutop  24123  restutopopn  24124  ucncn  24170  cfilufg  24178  trcfilu  24179  psmet0  24194  psmettri2  24195  prdsxmetlem  24254  prdsbl  24377  prdsxmslem2  24415  psmetutop  24453  cnmpt2ds  24730  bndth  24855  cnmpt2ip  25146  iscmet3lem2  25190  cmetcusp1  25251  rrxcph  25290  ovoliunlem1  25401  ovoliunlem3  25403  ovoliun  25404  ovoliun2  25405  ovolscalem1  25412  volfiniun  25446  uniioombllem4  25485  mbfeqalem1  25540  mbfres2  25544  ismbf3d  25553  mbfsup  25563  mbfinf  25564  mbflim  25567  itg1ge0  25585  itg1mulc  25603  itg1climres  25613  mbfi1fseqlem4  25617  itg2lea  25643  itg2splitlem  25647  itg2split  25648  itg2monolem1  25649  itg2mono  25652  itg2i1fseqle  25653  itg2i1fseq  25654  itg2addlem  25657  itg2cnlem1  25660  itgeqa  25713  itgfsum  25726  itgabs  25734  itggt0  25743  dvlipcn  25897  dvfsumabs  25927  dvfsumlem2  25931  dvfsumlem2OLD  25932  itgsubstlem  25953  coeeulem  26127  dgrlem  26132  dgrlb  26139  coeaddlem  26152  coecj  26182  coecjOLD  26184  ulmss  26304  leibpi  26850  xrlimcnp  26876  o1cxp  26883  jensen  26897  lgambdd  26945  wilthlem2  26977  sqff1o  27090  fsumdvdscom  27093  fsumdvdsmul  27103  fsumdvdsmulOLD  27105  dchrmulcl  27158  dchrmullid  27161  dchrinv  27170  dchrvmasumlem2  27407  ostth1  27542  conway  27710  slerec  27730  ercgrg  28462  f1otrg  28816  f1otrge  28817  ubthlem2  30815  fmptcof2  32600  disjdsct  32645  fprodex01  32770  prodindf  32806  ccatf1  32890  ressprs  32908  mgcf1o  32945  chnccats1  32957  gsumpart  33010  archiabl  33140  lmodslmd  33146  elrgspnlem1  33182  elrgspnlem2  33183  elrgspnsubrunlem2  33188  rhmimaidl  33369  gsummoncoe1fzo  33530  ply1gsumz  33531  fedgmullem2  33597  fedgmul  33598  txomap  33801  qtophaus  33803  locfinreflem  33807  ordtrest2NEWlem  33889  lmdvg  33920  zrhcntr  33946  esumcl  33997  esumeq2d  34004  esumnul  34015  hasheuni  34052  esumcvg  34053  esumcvgre  34058  insiga  34104  ldsysgenld  34127  ldgenpisyslem1  34130  measvunilem  34179  measvunilem0  34180  measdivcstALTV  34192  cntmeas  34193  voliune  34196  volfiniune  34197  1stmbfm  34228  2ndmbfm  34229  omssubadd  34268  difelcarsg  34278  inelcarsg  34279  eulerpartlems  34328  eulerpartlemsv3  34329  eulerpartlemgvv  34344  dstrvprob  34440  hashreprin  34588  reprgt  34589  breprexplemc  34600  circlemeth  34608  hgt750lema  34625  tgoldbachgtd  34630  bnj93  34830  bnj518  34853  bnj1489  35023  fnrelpredd  35056  subfacp1lem3  35155  subfacp1lem5  35157  erdszelem8  35171  ptpconn  35206  resconn  35219  cvmliftmolem2  35255  cvmlift2lem11  35286  cvmliftphtlem  35290  mclsax  35542  weiunfr  36441  fin2so  37587  poimirlem18  37618  poimirlem21  37621  mblfinlem2  37638  itgabsnc  37669  itggt0cn  37670  prdsbnd  37773  prdstotbnd  37774  prdsbnd2  37775  rrnequiv  37815  eqlkr3  39080  dih1dimatlem  41308  3factsumint  41998  aks6d1c5lem2  42111  fnwe2lem1  43023  cantnf2  43298  nadd1suc  43365  imo72b2  44145  rfcnnnub  45014  disjxp1  45047  disjinfi  45170  fvixp2  45177  dmrelrnrel  45204  fvmptelcdmf  45248  suplesup  45319  infxr  45346  monoord2xrv  45462  climinf  45587  climsuse  45589  mullimc  45597  limccog  45601  mullimcf  45604  limcperiod  45609  limcleqr  45625  neglimc  45628  0ellimcdiv  45630  limclner  45632  limsuppnfdlem  45682  limsupubuzlem  45693  xlimmnfvlem2  45814  xlimpnfvlem2  45818  climxlim2lem  45826  dvdivbd  45904  ioodvbdlimc1lem1  45912  dvnprodlem2  45928  iblsplit  45947  stoweidlem5  45986  stoweidlem16  45997  stoweidlem21  46002  stoweidlem24  46005  stoweidlem25  46006  stoweidlem28  46009  stoweidlem31  46012  stoweidlem41  46022  stoweidlem42  46023  stoweidlem44  46025  stoweidlem45  46026  stoweidlem48  46029  stoweidlem51  46032  stoweidlem54  46035  stoweidlem57  46038  stoweidlem60  46041  stoweidlem62  46043  stirlinglem5  46059  dirkercncflem3  46086  fourierdlem11  46099  fourierdlem12  46100  fourierdlem14  46102  fourierdlem15  46103  fourierdlem31  46119  fourierdlem34  46122  fourierdlem41  46129  fourierdlem48  46135  fourierdlem49  46136  fourierdlem50  46137  fourierdlem54  46141  fourierdlem69  46156  fourierdlem73  46160  fourierdlem74  46161  fourierdlem75  46162  fourierdlem76  46163  fourierdlem79  46166  fourierdlem80  46167  fourierdlem81  46168  fourierdlem92  46179  fourierdlem93  46180  fourierdlem94  46181  fourierdlem97  46184  fourierdlem103  46190  fourierdlem104  46191  fourierdlem111  46198  fourierdlem113  46200  etransclem32  46247  subsaliuncllem  46338  sge0rpcpnf  46402  caragendifcl  46495  iinhoiicclem  46654  pimdecfgtioc  46696  issmfgtlem  46736  ormklocald  46855  ormkglobd  46856  initopropd  49228  termopropd  49229  thincciso2  49440