Theorem r19.21bi 3230

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053

This theorem is referenced by:  r19.21be  3231  rspec2  3257  rspec3  3258  ralxfr2d  5348  fvmptelcdm  7060  fompt  7065  f1oresrab  7075  isoselem  7290  mpoexw  8025  naddsuc2  8631  boxcutc  8883  xpf1o  9071  fineqvlem  9170  indexfi  9264  dffi3  9338  suppr  9379  supiso  9383  infpr  9412  ordtypelem9  9435  brwdom3  9491  xpwdomg  9494  ixpiunwdom  9499  infxpenc2lem1  9935  hsmexlem4  10345  gchina  10616  wunom  10637  prcdnq  10910  prnmax  10912  dedekind  11303  dedekindle  11304  monoord2  13989  limsupgre  15437  limsupbnd1  15438  limsupbnd2  15439  climmpt2  15529  rlimcld2  15534  climsup  15626  sumpr  15704  sumtp  15705  fsum2dlem  15726  fsumiun  15778  fprod2dlem  15939  iserodd  16800  vdwlem1  16946  vdwlem6  16951  vdwnnlem3  16962  imasvscafn  17495  fuciso  17939  evlfcl  18182  yonedainv  18241  oduprs  18260  acsmapd  18514  chnccats1  18585  chnccat  18586  prdsmndd  18732  psgnunilem5  19463  gsummpt1n0  19934  dprdspan  19998  ablfaclem2  20057  srgdilem  20167  srgrz  20182  srglz  20183  issrngd  20826  frgpcyg  21566  psrbaglesupp  21915  psrbagcon  21918  psrbagleadd1  21921  evlslem2  22070  mpfind  22106  psdmul  22145  ply1chr  22284  gsumsmonply1  22285  gsummoncoe1  22286  evl1gsummon  22343  cpmatmcllem  22696  neiptoptop  23109  neiptopnei  23110  ordtrest2lem  23181  cncmp  23370  1stckgenlem  23531  ptcld  23591  dfac14  23596  ptcnplem  23599  pthaus  23616  xkococnlem  23637  xkococn  23638  cnmpt2k  23666  xpstopnlem1  23787  cnpflfi  23977  ptcmplem2  24031  cnextcn  24045  cnextfres1  24046  cnmpt2plusg  24066  cnmpt2vsca  24173  ustfilxp  24191  utoptop  24212  restutop  24215  restutopopn  24216  ucncn  24262  cfilufg  24270  trcfilu  24271  psmet0  24286  psmettri2  24287  prdsxmetlem  24346  prdsbl  24469  prdsxmslem2  24507  psmetutop  24545  cnmpt2ds  24822  bndth  24938  cnmpt2ip  25228  iscmet3lem2  25272  cmetcusp1  25333  rrxcph  25372  ovoliunlem1  25482  ovoliunlem3  25484  ovoliun  25485  ovoliun2  25486  ovolscalem1  25493  volfiniun  25527  uniioombllem4  25566  mbfeqalem1  25621  mbfres2  25625  ismbf3d  25634  mbfsup  25644  mbfinf  25645  mbflim  25648  itg1ge0  25666  itg1mulc  25684  itg1climres  25694  mbfi1fseqlem4  25698  itg2lea  25724  itg2splitlem  25728  itg2split  25729  itg2monolem1  25730  itg2mono  25733  itg2i1fseqle  25734  itg2i1fseq  25735  itg2addlem  25738  itg2cnlem1  25741  itgeqa  25794  itgfsum  25807  itgabs  25815  itggt0  25824  dvlipcn  25974  dvfsumabs  26003  dvfsumlem2  26007  itgsubstlem  26028  coeeulem  26202  dgrlem  26207  dgrlb  26214  coeaddlem  26227  coecj  26256  coecjOLD  26258  ulmss  26378  leibpi  26922  xrlimcnp  26948  o1cxp  26955  jensen  26969  lgambdd  27017  wilthlem2  27049  sqff1o  27162  fsumdvdscom  27165  fsumdvdsmul  27175  dchrmulcl  27229  dchrmullid  27232  dchrinv  27241  dchrvmasumlem2  27478  ostth1  27613  conway  27788  lesrec  27808  ercgrg  28602  f1otrg  28956  f1otrge  28957  ubthlem2  30960  fmptcof2  32748  disjdsct  32794  fprodex01  32916  prodindf  32940  ccatf1  33027  ressprs  33044  mgcf1o  33081  gsumpart  33142  suppgsumssiun  33151  archiabl  33277  lmodslmd  33283  elrgspnlem1  33321  elrgspnlem2  33322  elrgspnsubrunlem2  33327  rhmimaidl  33510  gsummoncoe1fzo  33675  ply1gsumz  33677  vietadeg1  33740  vietalem  33741  fedgmullem2  33793  fedgmul  33794  txomap  33997  qtophaus  33999  locfinreflem  34003  ordtrest2NEWlem  34085  lmdvg  34116  zrhcntr  34142  esumcl  34193  esumeq2d  34200  esumnul  34211  hasheuni  34248  esumcvg  34249  esumcvgre  34254  insiga  34300  ldsysgenld  34323  ldgenpisyslem1  34326  measvunilem  34375  measvunilem0  34376  measdivcstALTV  34388  cntmeas  34389  voliune  34392  volfiniune  34393  1stmbfm  34423  2ndmbfm  34424  omssubadd  34463  difelcarsg  34473  inelcarsg  34474  eulerpartlems  34523  eulerpartlemsv3  34524  eulerpartlemgvv  34539  dstrvprob  34635  hashreprin  34783  reprgt  34784  breprexplemc  34795  circlemeth  34803  hgt750lema  34820  tgoldbachgtd  34825  bnj93  35024  bnj518  35047  bnj1489  35217  fnrelpredd  35253  subfacp1lem3  35383  subfacp1lem5  35385  erdszelem8  35399  ptpconn  35434  resconn  35447  cvmliftmolem2  35483  cvmlift2lem11  35514  cvmliftphtlem  35518  mclsax  35770  weiunfr  36668  fin2so  37945  poimirlem18  37976  poimirlem21  37979  mblfinlem2  37996  itgabsnc  38027  itggt0cn  38028  prdsbnd  38131  prdstotbnd  38132  prdsbnd2  38133  rrnequiv  38173  eqlkr3  39564  dih1dimatlem  41792  3factsumint  42481  aks6d1c5lem2  42594  fnwe2lem1  43499  cantnf2  43774  nadd1suc  43841  imo72b2  44620  rfcnnnub  45488  disjxp1  45521  disjinfi  45643  fvixp2  45649  dmrelrnrel  45676  fvmptelcdmf  45720  suplesup  45790  infxr  45817  monoord2xrv  45932  climinf  46057  climsuse  46059  mullimc  46067  limccog  46071  mullimcf  46074  limcperiod  46079  limcleqr  46093  neglimc  46096  0ellimcdiv  46098  limclner  46100  limsuppnfdlem  46150  limsupubuzlem  46161  xlimmnfvlem2  46282  xlimpnfvlem2  46286  climxlim2lem  46294  dvdivbd  46372  ioodvbdlimc1lem1  46380  dvnprodlem2  46396  iblsplit  46415  stoweidlem5  46454  stoweidlem16  46465  stoweidlem21  46470  stoweidlem24  46473  stoweidlem25  46474  stoweidlem28  46477  stoweidlem31  46480  stoweidlem41  46490  stoweidlem42  46491  stoweidlem44  46493  stoweidlem45  46494  stoweidlem48  46497  stoweidlem51  46500  stoweidlem54  46503  stoweidlem57  46506  stoweidlem60  46509  stoweidlem62  46511  stirlinglem5  46527  dirkercncflem3  46554  fourierdlem11  46567  fourierdlem12  46568  fourierdlem14  46570  fourierdlem15  46571  fourierdlem31  46587  fourierdlem34  46590  fourierdlem41  46597  fourierdlem48  46603  fourierdlem49  46604  fourierdlem50  46605  fourierdlem54  46609  fourierdlem69  46624  fourierdlem73  46628  fourierdlem74  46629  fourierdlem75  46630  fourierdlem76  46631  fourierdlem79  46634  fourierdlem80  46635  fourierdlem81  46636  fourierdlem92  46647  fourierdlem93  46648  fourierdlem94  46649  fourierdlem97  46652  fourierdlem103  46658  fourierdlem104  46659  fourierdlem111  46666  fourierdlem113  46668  etransclem32  46715  subsaliuncllem  46806  sge0rpcpnf  46870  caragendifcl  46963  iinhoiicclem  47122  pimdecfgtioc  47164  issmfgtlem  47204  ormklocald  47323  ormkglobd  47324  initopropd  49733  termopropd  49734  thincciso2  49945