Theorem r19.21bi 3257

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068

This theorem is referenced by:  r19.21be  3258  rspec2  3285  rspec3  3286  ralxfr2d  5428  fvmptelcdm  7147  fompt  7152  f1oresrab  7161  isoselem  7377  mpoexw  8119  naddsuc2  8757  boxcutc  8999  xpf1o  9205  fineqvlem  9325  indexfi  9430  dffi3  9500  suppr  9540  supiso  9544  infpr  9572  ordtypelem9  9595  brwdom3  9651  xpwdomg  9654  ixpiunwdom  9659  infxpenc2lem1  10088  hsmexlem4  10498  gchina  10768  wunom  10789  prcdnq  11062  prnmax  11064  dedekind  11453  dedekindle  11454  monoord2  14084  limsupgre  15527  limsupbnd1  15528  limsupbnd2  15529  climmpt2  15619  rlimcld2  15624  climsup  15718  sumpr  15796  sumtp  15797  fsum2dlem  15818  fsumiun  15869  fprod2dlem  16028  iserodd  16882  vdwlem1  17028  vdwlem6  17033  vdwnnlem3  17044  imasvscafn  17597  fuciso  18045  evlfcl  18292  yonedainv  18351  acsmapd  18624  prdsmndd  18805  psgnunilem5  19536  gsummpt1n0  20007  dprdspan  20071  ablfaclem2  20130  srgdilem  20219  srgrz  20234  srglz  20235  issrngd  20878  frgpcyg  21615  psrbaglesupp  21965  psrbagcon  21968  psrbagleadd1  21971  evlslem2  22126  mpfind  22154  psdmul  22193  ply1chr  22331  gsumsmonply1  22332  gsummoncoe1  22333  evl1gsummon  22390  cpmatmcllem  22745  neiptoptop  23160  neiptopnei  23161  ordtrest2lem  23232  cncmp  23421  1stckgenlem  23582  ptcld  23642  dfac14  23647  ptcnplem  23650  pthaus  23667  xkococnlem  23688  xkococn  23689  cnmpt2k  23717  xpstopnlem1  23838  cnpflfi  24028  ptcmplem2  24082  cnextcn  24096  cnextfres1  24097  cnmpt2plusg  24117  cnmpt2vsca  24224  ustfilxp  24242  utoptop  24264  restutop  24267  restutopopn  24268  ucncn  24315  cfilufg  24323  trcfilu  24324  psmet0  24339  psmettri2  24340  prdsxmetlem  24399  prdsbl  24525  prdsxmslem2  24563  psmetutop  24601  cnmpt2ds  24884  bndth  25009  cnmpt2ip  25301  iscmet3lem2  25345  cmetcusp1  25406  rrxcph  25445  ovoliunlem1  25556  ovoliunlem3  25558  ovoliun  25559  ovoliun2  25560  ovolscalem1  25567  volfiniun  25601  uniioombllem4  25640  mbfeqalem1  25695  mbfres2  25699  ismbf3d  25708  mbfsup  25718  mbfinf  25719  mbflim  25722  itg1ge0  25740  itg1mulc  25759  itg1climres  25769  mbfi1fseqlem4  25773  itg2lea  25799  itg2splitlem  25803  itg2split  25804  itg2monolem1  25805  itg2mono  25808  itg2i1fseqle  25809  itg2i1fseq  25810  itg2addlem  25813  itg2cnlem1  25816  itgeqa  25869  itgfsum  25882  itgabs  25890  itggt0  25899  dvlipcn  26053  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  itgsubstlem  26109  coeeulem  26283  dgrlem  26288  dgrlb  26295  coeaddlem  26308  coecj  26338  ulmss  26458  leibpi  27003  xrlimcnp  27029  o1cxp  27036  jensen  27050  lgambdd  27098  wilthlem2  27130  sqff1o  27243  fsumdvdscom  27246  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  dchrmulcl  27311  dchrmullid  27314  dchrinv  27323  dchrvmasumlem2  27560  ostth1  27695  conway  27862  slerec  27882  ercgrg  28543  f1otrg  28897  f1otrge  28898  ubthlem2  30903  fmptcof2  32675  disjdsct  32714  fprodex01  32829  ccatf1  32915  ressprs  32936  oduprs  32937  mgcf1o  32976  gsumpart  33038  archiabl  33178  lmodslmd  33183  rhmimaidl  33425  gsummoncoe1fzo  33583  ply1gsumz  33584  fedgmullem2  33643  fedgmul  33644  txomap  33780  qtophaus  33782  locfinreflem  33786  ordtrest2NEWlem  33868  lmdvg  33899  prodindf  33987  esumcl  33994  esumeq2d  34001  esumnul  34012  hasheuni  34049  esumcvg  34050  esumcvgre  34055  insiga  34101  ldsysgenld  34124  ldgenpisyslem1  34127  measvunilem  34176  measvunilem0  34177  measdivcstALTV  34189  cntmeas  34190  voliune  34193  volfiniune  34194  1stmbfm  34225  2ndmbfm  34226  omssubadd  34265  difelcarsg  34275  inelcarsg  34276  eulerpartlems  34325  eulerpartlemsv3  34326  eulerpartlemgvv  34341  dstrvprob  34436  hashreprin  34597  reprgt  34598  breprexplemc  34609  circlemeth  34617  hgt750lema  34634  tgoldbachgtd  34639  bnj93  34839  bnj518  34862  bnj1489  35032  fnrelpredd  35065  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem8  35166  ptpconn  35201  resconn  35214  cvmliftmolem2  35250  cvmlift2lem11  35281  cvmliftphtlem  35285  mclsax  35537  weiunfr  36433  fin2so  37567  poimirlem18  37598  poimirlem21  37601  mblfinlem2  37618  itgabsnc  37649  itggt0cn  37650  prdsbnd  37753  prdstotbnd  37754  prdsbnd2  37755  rrnequiv  37795  eqlkr3  39057  dih1dimatlem  41286  3factsumint  41982  aks6d1c5lem2  42095  fnwe2lem1  43007  cantnf2  43287  nadd1suc  43354  imo72b2  44134  rfcnnnub  44936  disjxp1  44971  disjinfi  45099  fvixp2  45106  dmrelrnrel  45133  fvmptelcdmf  45180  suplesup  45254  infxr  45282  monoord2xrv  45399  climinf  45527  climsuse  45529  mullimc  45537  limccog  45541  mullimcf  45544  limcperiod  45549  limcleqr  45565  neglimc  45568  0ellimcdiv  45570  limclner  45572  limsuppnfdlem  45622  limsupubuzlem  45633  xlimmnfvlem2  45754  xlimpnfvlem2  45758  climxlim2lem  45766  dvdivbd  45844  ioodvbdlimc1lem1  45852  dvnprodlem2  45868  iblsplit  45887  stoweidlem5  45926  stoweidlem16  45937  stoweidlem21  45942  stoweidlem24  45945  stoweidlem25  45946  stoweidlem28  45949  stoweidlem31  45952  stoweidlem41  45962  stoweidlem42  45963  stoweidlem44  45965  stoweidlem45  45966  stoweidlem48  45969  stoweidlem51  45972  stoweidlem54  45975  stoweidlem57  45978  stoweidlem60  45981  stoweidlem62  45983  stirlinglem5  45999  dirkercncflem3  46026  fourierdlem11  46039  fourierdlem12  46040  fourierdlem14  46042  fourierdlem15  46043  fourierdlem31  46059  fourierdlem34  46062  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem54  46081  fourierdlem69  46096  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem79  46106  fourierdlem80  46107  fourierdlem81  46108  fourierdlem92  46119  fourierdlem93  46120  fourierdlem94  46121  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem113  46140  etransclem32  46187  subsaliuncllem  46278  sge0rpcpnf  46342  caragendifcl  46435  iinhoiicclem  46594  pimdecfgtioc  46636  issmfgtlem  46676