Theorem r19.21bi 3228

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3052

This theorem is referenced by:  r19.21be  3229  rspec2  3255  rspec3  3256  ralxfr2d  5355  fvmptelcdm  7058  fompt  7063  f1oresrab  7072  isoselem  7287  mpoexw  8022  naddsuc2  8629  boxcutc  8879  xpf1o  9067  fineqvlem  9166  indexfi  9260  dffi3  9334  suppr  9375  supiso  9379  infpr  9408  ordtypelem9  9431  brwdom3  9487  xpwdomg  9490  ixpiunwdom  9495  infxpenc2lem1  9929  hsmexlem4  10339  gchina  10610  wunom  10631  prcdnq  10904  prnmax  10906  dedekind  11296  dedekindle  11297  monoord2  13956  limsupgre  15404  limsupbnd1  15405  limsupbnd2  15406  climmpt2  15496  rlimcld2  15501  climsup  15593  sumpr  15671  sumtp  15672  fsum2dlem  15693  fsumiun  15744  fprod2dlem  15903  iserodd  16763  vdwlem1  16909  vdwlem6  16914  vdwnnlem3  16925  imasvscafn  17458  fuciso  17902  evlfcl  18145  yonedainv  18204  oduprs  18223  acsmapd  18477  chnccats1  18548  chnccat  18549  prdsmndd  18695  psgnunilem5  19423  gsummpt1n0  19894  dprdspan  19958  ablfaclem2  20017  srgdilem  20127  srgrz  20142  srglz  20143  issrngd  20788  frgpcyg  21528  psrbaglesupp  21878  psrbagcon  21881  psrbagleadd1  21884  evlslem2  22034  mpfind  22070  psdmul  22109  ply1chr  22250  gsumsmonply1  22251  gsummoncoe1  22252  evl1gsummon  22309  cpmatmcllem  22662  neiptoptop  23075  neiptopnei  23076  ordtrest2lem  23147  cncmp  23336  1stckgenlem  23497  ptcld  23557  dfac14  23562  ptcnplem  23565  pthaus  23582  xkococnlem  23603  xkococn  23604  cnmpt2k  23632  xpstopnlem1  23753  cnpflfi  23943  ptcmplem2  23997  cnextcn  24011  cnextfres1  24012  cnmpt2plusg  24032  cnmpt2vsca  24139  ustfilxp  24157  utoptop  24178  restutop  24181  restutopopn  24182  ucncn  24228  cfilufg  24236  trcfilu  24237  psmet0  24252  psmettri2  24253  prdsxmetlem  24312  prdsbl  24435  prdsxmslem2  24473  psmetutop  24511  cnmpt2ds  24788  bndth  24913  cnmpt2ip  25204  iscmet3lem2  25248  cmetcusp1  25309  rrxcph  25348  ovoliunlem1  25459  ovoliunlem3  25461  ovoliun  25462  ovoliun2  25463  ovolscalem1  25470  volfiniun  25504  uniioombllem4  25543  mbfeqalem1  25598  mbfres2  25602  ismbf3d  25611  mbfsup  25621  mbfinf  25622  mbflim  25625  itg1ge0  25643  itg1mulc  25661  itg1climres  25671  mbfi1fseqlem4  25675  itg2lea  25701  itg2splitlem  25705  itg2split  25706  itg2monolem1  25707  itg2mono  25710  itg2i1fseqle  25711  itg2i1fseq  25712  itg2addlem  25715  itg2cnlem1  25718  itgeqa  25771  itgfsum  25784  itgabs  25792  itggt0  25801  dvlipcn  25955  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  itgsubstlem  26011  coeeulem  26185  dgrlem  26190  dgrlb  26197  coeaddlem  26210  coecj  26240  coecjOLD  26242  ulmss  26362  leibpi  26908  xrlimcnp  26934  o1cxp  26941  jensen  26955  lgambdd  27003  wilthlem2  27035  sqff1o  27148  fsumdvdscom  27151  fsumdvdsmul  27161  fsumdvdsmulOLD  27163  dchrmulcl  27216  dchrmullid  27219  dchrinv  27228  dchrvmasumlem2  27465  ostth1  27600  conway  27775  lesrec  27795  ercgrg  28589  f1otrg  28943  f1otrge  28944  ubthlem2  30946  fmptcof2  32735  disjdsct  32782  fprodex01  32906  prodindf  32944  ccatf1  33031  ressprs  33048  mgcf1o  33085  gsumpart  33146  archiabl  33280  lmodslmd  33286  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnsubrunlem2  33330  rhmimaidl  33513  gsummoncoe1fzo  33678  ply1gsumz  33680  vietadeg1  33734  vietalem  33735  fedgmullem2  33787  fedgmul  33788  txomap  33991  qtophaus  33993  locfinreflem  33997  ordtrest2NEWlem  34079  lmdvg  34110  zrhcntr  34136  esumcl  34187  esumeq2d  34194  esumnul  34205  hasheuni  34242  esumcvg  34243  esumcvgre  34248  insiga  34294  ldsysgenld  34317  ldgenpisyslem1  34320  measvunilem  34369  measvunilem0  34370  measdivcstALTV  34382  cntmeas  34383  voliune  34386  volfiniune  34387  1stmbfm  34417  2ndmbfm  34418  omssubadd  34457  difelcarsg  34467  inelcarsg  34468  eulerpartlems  34517  eulerpartlemsv3  34518  eulerpartlemgvv  34533  dstrvprob  34629  hashreprin  34777  reprgt  34778  breprexplemc  34789  circlemeth  34797  hgt750lema  34814  tgoldbachgtd  34819  bnj93  35019  bnj518  35042  bnj1489  35212  fnrelpredd  35247  subfacp1lem3  35376  subfacp1lem5  35378  erdszelem8  35392  ptpconn  35427  resconn  35440  cvmliftmolem2  35476  cvmlift2lem11  35507  cvmliftphtlem  35511  mclsax  35763  weiunfr  36661  fin2so  37808  poimirlem18  37839  poimirlem21  37842  mblfinlem2  37859  itgabsnc  37890  itggt0cn  37891  prdsbnd  37994  prdstotbnd  37995  prdsbnd2  37996  rrnequiv  38036  eqlkr3  39361  dih1dimatlem  41589  3factsumint  42279  aks6d1c5lem2  42392  fnwe2lem1  43292  cantnf2  43567  nadd1suc  43634  imo72b2  44413  rfcnnnub  45281  disjxp1  45314  disjinfi  45436  fvixp2  45443  dmrelrnrel  45470  fvmptelcdmf  45514  suplesup  45584  infxr  45611  monoord2xrv  45727  climinf  45852  climsuse  45854  mullimc  45862  limccog  45866  mullimcf  45869  limcperiod  45874  limcleqr  45888  neglimc  45891  0ellimcdiv  45893  limclner  45895  limsuppnfdlem  45945  limsupubuzlem  45956  xlimmnfvlem2  46077  xlimpnfvlem2  46081  climxlim2lem  46089  dvdivbd  46167  ioodvbdlimc1lem1  46175  dvnprodlem2  46191  iblsplit  46210  stoweidlem5  46249  stoweidlem16  46260  stoweidlem21  46265  stoweidlem24  46268  stoweidlem25  46269  stoweidlem28  46272  stoweidlem31  46275  stoweidlem41  46285  stoweidlem42  46286  stoweidlem44  46288  stoweidlem45  46289  stoweidlem48  46292  stoweidlem51  46295  stoweidlem54  46298  stoweidlem57  46301  stoweidlem60  46304  stoweidlem62  46306  stirlinglem5  46322  dirkercncflem3  46349  fourierdlem11  46362  fourierdlem12  46363  fourierdlem14  46365  fourierdlem15  46366  fourierdlem31  46382  fourierdlem34  46385  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem54  46404  fourierdlem69  46419  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem79  46429  fourierdlem80  46430  fourierdlem81  46431  fourierdlem92  46442  fourierdlem93  46443  fourierdlem94  46444  fourierdlem97  46447  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem113  46463  etransclem32  46510  subsaliuncllem  46601  sge0rpcpnf  46665  caragendifcl  46758  iinhoiicclem  46917  pimdecfgtioc  46959  issmfgtlem  46999  ormklocald  47118  ormkglobd  47119  initopropd  49488  termopropd  49489  thincciso2  49700