Theorem r19.21bi 3254

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-ral 3077

This theorem is referenced by:  r19.21be  3255  rspec2  3281  rspec3  3282  ralxfr2d  5367  fvmptelcdm  7094  fompt  7099  f1oresrab  7109  isoselem  7325  mpoexw  8059  naddsuc2  8672  boxcutc  8923  xpf1o  9111  fineqvlem  9210  indexfi  9303  dffi3  9377  suppr  9418  supiso  9422  infpr  9451  ordtypelem9  9474  brwdom3  9530  xpwdomg  9533  ixpiunwdom  9538  infxpenc2lem1  9975  hsmexlem4  10386  gchina  10657  wunom  10678  prcdnq  10951  prnmax  10953  dedekind  11346  dedekindle  11347  monoord2  14046  limsupgre  15508  limsupbnd1  15509  limsupbnd2  15510  climmpt2  15600  rlimcld2  15605  climsup  15697  sumpr  15775  sumtp  15776  fsum2dlem  15797  fsumiun  15849  fprod2dlem  16010  iserodd  16871  vdwlem1  17017  vdwlem6  17022  vdwnnlem3  17033  imasvscafn  17567  fuciso  18011  evlfcl  18254  yonedainv  18313  oduprs  18332  acsmapd  18586  chnccats1  18657  chnccat  18658  prdsmndd  18804  psgnunilem5  19534  gsummpt1n0  20005  dprdspan  20069  ablfaclem2  20128  srgdilem  20242  srgrz  20257  srglz  20258  issrngd  20904  frgpcyg  21625  psrbaglesupp  21974  psrbagcon  21977  psrbagleadd1  21980  evlslem2  22132  mpfind  22168  psdmul  22231  ply1chr  22369  gsumsmonply1  22370  gsummoncoe1  22371  evl1gsummon  22428  cpmatmcllem  22778  neiptoptop  23191  neiptopnei  23192  ordtrest2lem  23263  cncmp  23452  1stckgenlem  23613  ptcld  23673  dfac14  23678  ptcnplem  23681  pthaus  23698  xkococnlem  23719  xkococn  23720  cnmpt2k  23748  xpstopnlem1  23869  cnpflfi  24059  ptcmplem2  24113  cnextcn  24127  cnextfres1  24128  cnmpt2plusg  24148  cnmpt2vsca  24255  ustfilxp  24273  utoptop  24294  restutop  24297  restutopopn  24298  ucncn  24344  cfilufg  24352  trcfilu  24353  psmet0  24368  psmettri2  24369  prdsxmetlem  24428  prdsbl  24551  prdsxmslem2  24589  psmetutop  24627  cnmpt2ds  24904  bndth  25020  cnmpt2ip  25310  iscmet3lem2  25354  cmetcusp1  25415  rrxcph  25454  ovoliunlem1  25564  ovoliunlem3  25566  ovoliun  25567  ovoliun2  25568  ovolscalem1  25575  volfiniun  25609  uniioombllem4  25648  mbfeqalem1  25703  mbfres2  25707  ismbf3d  25716  mbfsup  25726  mbfinf  25727  mbflim  25730  itg1ge0  25748  itg1mulc  25766  itg1climres  25776  mbfi1fseqlem4  25780  itg2lea  25806  itg2splitlem  25810  itg2split  25811  itg2monolem1  25812  itg2mono  25815  itg2i1fseqle  25816  itg2i1fseq  25817  itg2addlem  25820  itg2cnlem1  25823  itgeqa  25876  itgfsum  25889  itgabs  25897  itggt0  25906  dvlipcn  26056  dvfsumabs  26085  dvfsumlem2  26089  itgsubstlem  26110  coeeulem  26284  dgrlem  26289  dgrlb  26296  coeaddlem  26309  coecj  26338  coecjOLD  26340  ulmss  26460  leibpi  27007  xrlimcnp  27033  o1cxp  27039  jensen  27053  lgambdd  27101  wilthlem2  27133  sqff1o  27246  fsumdvdscom  27249  fsumdvdsmul  27259  dchrmulcl  27313  dchrmullid  27316  dchrinv  27325  dchrvmasumlem2  27562  ostth1  27697  conway  27872  lesrec  27892  ercgrg  28686  f1otrg  29071  f1otrge  29072  ubthlem2  31074  fmptcof2  32859  disjdsct  32905  fprodex01  33027  prodindf  33040  ccatf1  33127  ressprs  33144  mgcf1o  33181  gsumpart  33243  suppgsumssiun  33252  archiabl  33378  lmodslmd  33384  elrgspnlem1  33423  elrgspnlem2  33424  elrgspnsubrunlem2  33429  rhmimaidl  33618  gsummoncoe1fzo  33793  ply1gsumz  33795  vietadeg1  33875  vietalem  33876  fedgmullem2  33927  fedgmul  33928  txomap  34131  qtophaus  34133  locfinreflem  34137  ordtrest2NEWlem  34219  lmdvg  34250  zrhcntr  34276  esumcl  34327  esumeq2d  34334  esumnul  34345  hasheuni  34382  esumcvg  34383  esumcvgre  34388  insiga  34434  ldsysgenld  34457  ldgenpisyslem1  34460  measvunilem  34509  measvunilem0  34510  measdivcstALTV  34522  cntmeas  34523  voliune  34526  volfiniune  34527  1stmbfm  34557  2ndmbfm  34558  omssubadd  34597  difelcarsg  34607  inelcarsg  34608  eulerpartlems  34657  eulerpartlemsv3  34658  eulerpartlemgvv  34673  dstrvprob  34769  hashreprin  34914  reprgt  34915  breprexplemc  34926  circlemeth  34934  hgt750lema  34951  tgoldbachgtd  34956  bnj93  35158  bnj518  35181  bnj1489  35351  fnrelpredd  35387  subfacp1lem3  35532  subfacp1lem5  35534  erdszelem8  35548  ptpconn  35583  resconn  35596  cvmliftmolem2  35632  cvmlift2lem11  35663  cvmliftphtlem  35667  mclsax  35919  weiunfr  36827  fin2so  38106  poimirlem18  38137  poimirlem21  38140  mblfinlem2  38157  itgabsnc  38188  itggt0cn  38189  prdsbnd  38292  prdstotbnd  38293  prdsbnd2  38294  rrnequiv  38334  eqlkr3  39725  dih1dimatlem  41953  3factsumint  42642  aks6d1c5lem2  42755  fnwe2lem1  43627  cantnf2  43902  nadd1suc  43969  imo72b2  44748  rfcnnnub  45616  disjxp1  45649  disjinfi  45770  fvixp2  45776  dmrelrnrel  45802  fvmptelcdmf  45845  suplesup  45915  infxr  45942  monoord2xrv  46057  climinf  46182  climsuse  46184  mullimc  46192  limccog  46196  mullimcf  46199  limcperiod  46204  limcleqr  46218  neglimc  46221  0ellimcdiv  46223  limclner  46225  limsuppnfdlem  46275  limsupubuzlem  46286  xlimmnfvlem2  46407  xlimpnfvlem2  46411  climxlim2lem  46419  dvdivbd  46497  ioodvbdlimc1lem1  46505  dvnprodlem2  46521  iblsplit  46540  stoweidlem5  46579  stoweidlem16  46590  stoweidlem21  46595  stoweidlem24  46598  stoweidlem25  46599  stoweidlem28  46602  stoweidlem31  46605  stoweidlem41  46615  stoweidlem42  46616  stoweidlem44  46618  stoweidlem45  46619  stoweidlem48  46622  stoweidlem51  46625  stoweidlem54  46628  stoweidlem57  46631  stoweidlem60  46634  stoweidlem62  46636  stirlinglem5  46652  dirkercncflem3  46679  fourierdlem11  46692  fourierdlem12  46693  fourierdlem14  46695  fourierdlem15  46696  fourierdlem31  46712  fourierdlem34  46715  fourierdlem41  46722  fourierdlem48  46728  fourierdlem49  46729  fourierdlem50  46730  fourierdlem54  46734  fourierdlem69  46749  fourierdlem73  46753  fourierdlem74  46754  fourierdlem75  46755  fourierdlem76  46756  fourierdlem79  46759  fourierdlem80  46760  fourierdlem81  46761  fourierdlem92  46772  fourierdlem93  46773  fourierdlem94  46774  fourierdlem97  46777  fourierdlem103  46783  fourierdlem104  46784  fourierdlem111  46791  fourierdlem113  46793  etransclem32  46840  subsaliuncllem  46931  sge0rpcpnf  46995  caragendifcl  47088  iinhoiicclem  47247  pimdecfgtioc  47289  issmfgtlem  47329  ormklocald  47450  ormkglobd  47451  initopropd  49864  termopropd  49865  thincciso2  50076