Theorem r19.21bi 3243

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099  ∀wral 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-12 2164

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-ral 3057

This theorem is referenced by:  r19.21be  3244  rspec2  3271  rspec3  3272  ralxfr2d  5404  fvmptelcdm  7117  fompt  7122  f1oresrab  7130  isoselem  7343  mpoexw  8077  boxcutc  8951  xpf1o  9155  fineqvlem  9278  indexfi  9376  dffi3  9446  suppr  9486  supiso  9490  infpr  9518  ordtypelem9  9541  brwdom3  9597  xpwdomg  9600  ixpiunwdom  9605  infxpenc2lem1  10034  hsmexlem4  10444  gchina  10714  wunom  10735  prcdnq  11008  prnmax  11010  dedekind  11399  dedekindle  11400  monoord2  14022  limsupgre  15449  limsupbnd1  15450  limsupbnd2  15451  climmpt2  15541  rlimcld2  15546  climsup  15640  sumpr  15718  sumtp  15719  fsum2dlem  15740  fsumiun  15791  fprod2dlem  15948  iserodd  16795  vdwlem1  16941  vdwlem6  16946  vdwnnlem3  16957  imasvscafn  17510  fuciso  17958  evlfcl  18205  yonedainv  18264  acsmapd  18537  prdsmndd  18718  psgnunilem5  19440  gsummpt1n0  19911  dprdspan  19975  ablfaclem2  20034  srgdilem  20123  srgrz  20138  srglz  20139  issrngd  20730  frgpcyg  21494  psrbaglesupp  21844  psrbaglesuppOLD  21845  psrbagcon  21850  psrbagconOLD  21851  psrbagleadd1  21856  evlslem2  22012  mpfind  22040  psdmul  22077  ply1chr  22212  gsumsmonply1  22213  gsummoncoe1  22214  evl1gsummon  22271  cpmatmcllem  22607  neiptoptop  23022  neiptopnei  23023  ordtrest2lem  23094  cncmp  23283  1stckgenlem  23444  ptcld  23504  dfac14  23509  ptcnplem  23512  pthaus  23529  xkococnlem  23550  xkococn  23551  cnmpt2k  23579  xpstopnlem1  23700  cnpflfi  23890  ptcmplem2  23944  cnextcn  23958  cnextfres1  23959  cnmpt2plusg  23979  cnmpt2vsca  24086  ustfilxp  24104  utoptop  24126  restutop  24129  restutopopn  24130  ucncn  24177  cfilufg  24185  trcfilu  24186  psmet0  24201  psmettri2  24202  prdsxmetlem  24261  prdsbl  24387  prdsxmslem2  24425  psmetutop  24463  cnmpt2ds  24746  bndth  24871  cnmpt2ip  25163  iscmet3lem2  25207  cmetcusp1  25268  rrxcph  25307  ovoliunlem1  25418  ovoliunlem3  25420  ovoliun  25421  ovoliun2  25422  ovolscalem1  25429  volfiniun  25463  uniioombllem4  25502  mbfeqalem1  25557  mbfres2  25561  ismbf3d  25570  mbfsup  25580  mbfinf  25581  mbflim  25584  itg1ge0  25602  itg1mulc  25621  itg1climres  25631  mbfi1fseqlem4  25635  itg2lea  25661  itg2splitlem  25665  itg2split  25666  itg2monolem1  25667  itg2mono  25670  itg2i1fseqle  25671  itg2i1fseq  25672  itg2addlem  25675  itg2cnlem1  25678  itgeqa  25730  itgfsum  25743  itgabs  25751  itggt0  25760  dvlipcn  25914  dvfsumabs  25944  dvfsumlem2  25948  dvfsumlem2OLD  25949  itgsubstlem  25970  coeeulem  26145  dgrlem  26150  dgrlb  26157  coeaddlem  26170  coecj  26200  ulmss  26320  leibpi  26861  xrlimcnp  26887  o1cxp  26894  jensen  26908  lgambdd  26956  wilthlem2  26988  sqff1o  27101  fsumdvdscom  27104  fsumdvdsmul  27114  fsumdvdsmulOLD  27116  dchrmulcl  27169  dchrmullid  27172  dchrinv  27181  dchrvmasumlem2  27418  ostth1  27553  conway  27719  slerec  27739  ercgrg  28308  f1otrg  28662  f1otrge  28663  ubthlem2  30668  fmptcof2  32426  disjdsct  32466  fprodex01  32570  ccatf1  32654  ressprs  32672  oduprs  32673  mgcf1o  32712  gsumpart  32747  archiabl  32884  lmodslmd  32889  rhmimaidl  33083  gsummoncoe1fzo  33200  ply1gsumz  33201  fedgmullem2  33260  fedgmul  33261  txomap  33371  qtophaus  33373  locfinreflem  33377  ordtrest2NEWlem  33459  lmdvg  33490  prodindf  33578  esumcl  33585  esumeq2d  33592  esumnul  33603  hasheuni  33640  esumcvg  33641  esumcvgre  33646  insiga  33692  ldsysgenld  33715  ldgenpisyslem1  33718  measvunilem  33767  measvunilem0  33768  measdivcstALTV  33780  cntmeas  33781  voliune  33784  volfiniune  33785  1stmbfm  33816  2ndmbfm  33817  omssubadd  33856  difelcarsg  33866  inelcarsg  33867  eulerpartlems  33916  eulerpartlemsv3  33917  eulerpartlemgvv  33932  dstrvprob  34027  hashreprin  34188  reprgt  34189  breprexplemc  34200  circlemeth  34208  hgt750lema  34225  tgoldbachgtd  34230  bnj93  34430  bnj518  34453  bnj1489  34623  fnrelpredd  34648  subfacp1lem3  34728  subfacp1lem5  34730  erdszelem8  34744  ptpconn  34779  resconn  34792  cvmliftmolem2  34828  cvmlift2lem11  34859  cvmliftphtlem  34863  mclsax  35115  fin2so  37015  poimirlem18  37046  poimirlem21  37049  mblfinlem2  37066  itgabsnc  37097  itggt0cn  37098  prdsbnd  37201  prdstotbnd  37202  prdsbnd2  37203  rrnequiv  37243  eqlkr3  38510  dih1dimatlem  40739  3factsumint  41433  aks6d1c5lem2  41541  fnwe2lem1  42396  cantnf2  42677  nadd1suc  42744  naddsuc2  42745  imo72b2  43525  rfcnnnub  44321  disjxp1  44356  disjinfi  44488  fvixp2  44495  dmrelrnrel  44522  fvmptelcdmf  44570  suplesup  44644  infxr  44672  monoord2xrv  44789  climinf  44917  climsuse  44919  mullimc  44927  limccog  44931  mullimcf  44934  limcperiod  44939  limcleqr  44955  neglimc  44958  0ellimcdiv  44960  limclner  44962  limsuppnfdlem  45012  limsupubuzlem  45023  xlimmnfvlem2  45144  xlimpnfvlem2  45148  climxlim2lem  45156  dvdivbd  45234  ioodvbdlimc1lem1  45242  dvnprodlem2  45258  iblsplit  45277  stoweidlem5  45316  stoweidlem16  45327  stoweidlem21  45332  stoweidlem24  45335  stoweidlem25  45336  stoweidlem28  45339  stoweidlem31  45342  stoweidlem41  45352  stoweidlem42  45353  stoweidlem44  45355  stoweidlem45  45356  stoweidlem48  45359  stoweidlem51  45362  stoweidlem54  45365  stoweidlem57  45368  stoweidlem60  45371  stoweidlem62  45373  stirlinglem5  45389  dirkercncflem3  45416  fourierdlem11  45429  fourierdlem12  45430  fourierdlem14  45432  fourierdlem15  45433  fourierdlem31  45449  fourierdlem34  45452  fourierdlem41  45459  fourierdlem48  45465  fourierdlem49  45466  fourierdlem50  45467  fourierdlem54  45471  fourierdlem69  45486  fourierdlem73  45490  fourierdlem74  45491  fourierdlem75  45492  fourierdlem76  45493  fourierdlem79  45496  fourierdlem80  45497  fourierdlem81  45498  fourierdlem92  45509  fourierdlem93  45510  fourierdlem94  45511  fourierdlem97  45514  fourierdlem103  45520  fourierdlem104  45521  fourierdlem111  45528  fourierdlem113  45530  etransclem32  45577  subsaliuncllem  45668  sge0rpcpnf  45732  caragendifcl  45825  iinhoiicclem  45984  pimdecfgtioc  46026  issmfgtlem  46066