Theorem r19.21bi 3210

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∀wral 3140

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 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3145

This theorem is referenced by:  r19.21be  3212  rspec2  3213  rspec3  3214  ralxfr2d  5313  fvmptelrn  6879  f1oresrab  6891  isoselem  7096  mpoexw  7778  boxcutc  8507  xpf1o  8681  fineqvlem  8734  indexfi  8834  dffi3  8897  suppr  8937  supiso  8941  infpr  8969  ordtypelem9  8992  brwdom3  9048  xpwdomg  9051  ixpiunwdom  9057  infxpenc2lem1  9447  hsmexlem4  9853  gchina  10123  wunom  10144  prcdnq  10417  prnmax  10419  dedekind  10805  dedekindle  10806  monoord2  13404  limsupgre  14840  limsupbnd1  14841  limsupbnd2  14842  climmpt2  14932  rlimcld2  14937  climsup  15028  sumpr  15105  sumtp  15106  fsum2dlem  15127  fsumiun  15178  fprod2dlem  15336  iserodd  16174  vdwlem1  16319  vdwlem6  16324  vdwnnlem3  16335  imasvscafn  16812  fuciso  17247  evlfcl  17474  yonedainv  17533  acsmapd  17790  prdsmndd  17946  psgnunilem5  18624  gsummpt1n0  19087  dprdspan  19151  ablfaclem2  19210  srgi  19263  srgrz  19278  srglz  19279  issrngd  19634  psrbaglesupp  20150  psrbagcon  20153  evlslem2  20294  mpfind  20322  gsumsmonply1  20473  gsummoncoe1  20474  evl1gsummon  20530  frgpcyg  20722  cpmatmcllem  21328  neiptoptop  21741  neiptopnei  21742  ordtrest2lem  21813  cncmp  22002  1stckgenlem  22163  ptcld  22223  dfac14  22228  ptcnplem  22231  pthaus  22248  xkococnlem  22269  xkococn  22270  cnmpt2k  22298  xpstopnlem1  22419  cnpflfi  22609  ptcmplem2  22663  cnextcn  22677  cnextfres1  22678  cnmpt2plusg  22698  cnmpt2vsca  22805  ustfilxp  22823  utoptop  22845  restutop  22848  restutopopn  22849  ucncn  22896  cfilufg  22904  trcfilu  22905  psmet0  22920  psmettri2  22921  prdsxmetlem  22980  prdsbl  23103  prdsxmslem2  23141  psmetutop  23179  cnmpt2ds  23453  bndth  23564  cnmpt2ip  23853  iscmet3lem2  23897  cmetcusp1  23958  rrxcph  23997  ovoliunlem1  24105  ovoliunlem3  24107  ovoliun  24108  ovoliun2  24109  ovolscalem1  24116  volfiniun  24150  uniioombllem4  24189  mbfeqalem1  24244  mbfres2  24248  ismbf3d  24257  mbfsup  24267  mbfinf  24268  mbflim  24271  itg1ge0  24289  itg1mulc  24307  itg1climres  24317  mbfi1fseqlem4  24321  itg2lea  24347  itg2splitlem  24351  itg2split  24352  itg2monolem1  24353  itg2mono  24356  itg2i1fseqle  24357  itg2i1fseq  24358  itg2addlem  24361  itg2cnlem1  24364  itgeqa  24416  itgfsum  24429  itgabs  24437  itggt0  24444  dvlipcn  24593  dvfsumabs  24622  dvfsumlem2  24626  itgsubstlem  24647  coeeulem  24816  dgrlem  24821  dgrlb  24828  coeaddlem  24841  coecj  24870  ulmss  24987  leibpi  25522  xrlimcnp  25548  o1cxp  25554  jensen  25568  lgambdd  25616  wilthlem2  25648  sqff1o  25761  fsumdvdscom  25764  fsumdvdsmul  25774  dchrmulcl  25827  dchrmulid2  25830  dchrinv  25839  dchrvmasumlem2  26076  ostth1  26211  ercgrg  26305  f1otrg  26659  f1otrge  26660  ubthlem2  28650  fmptcof2  30404  disjdsct  30440  fprodex01  30543  ccatf1  30627  ressprs  30644  oduprs  30645  archiabl  30829  lmodslmd  30834  fedgmullem2  31028  fedgmul  31029  txomap  31100  qtophaus  31102  locfinreflem  31106  ordtrest2NEWlem  31167  lmdvg  31198  prodindf  31284  esumcl  31291  esumeq2d  31298  esumnul  31309  hasheuni  31346  esumcvg  31347  esumcvgre  31352  insiga  31398  ldsysgenld  31421  ldgenpisyslem1  31424  measvunilem  31473  measvunilem0  31474  measdivcstALTV  31486  cntmeas  31487  voliune  31490  volfiniune  31491  1stmbfm  31520  2ndmbfm  31521  omssubadd  31560  difelcarsg  31570  inelcarsg  31571  eulerpartlems  31620  eulerpartlemsv3  31621  eulerpartlemgvv  31636  dstrvprob  31731  hashreprin  31893  reprgt  31894  breprexplemc  31905  circlemeth  31913  hgt750lema  31930  tgoldbachgtd  31935  bnj93  32137  bnj518  32160  bnj1489  32330  subfacp1lem3  32431  subfacp1lem5  32433  erdszelem8  32447  ptpconn  32482  resconn  32495  cvmliftmolem2  32531  cvmlift2lem11  32562  cvmliftphtlem  32566  mclsax  32818  conway  33266  slerec  33279  fin2so  34881  poimirlem18  34912  poimirlem21  34915  mblfinlem2  34932  itgabsnc  34963  itggt0cn  34966  prdsbnd  35073  prdstotbnd  35074  prdsbnd2  35075  rrnequiv  35115  eqlkr3  36239  dih1dimatlem  38467  fnwe2lem1  39657  imo72b2  40532  rfcnnnub  41300  disjxp1  41338  fompt  41460  fvixp2  41468  dmrelrnrel  41497  suplesup  41614  infxr  41642  monoord2xrv  41767  climinf  41894  climsuse  41896  mullimc  41904  limccog  41908  mullimcf  41911  limcperiod  41916  limcleqr  41932  neglimc  41935  0ellimcdiv  41937  limclner  41939  limsuppnfdlem  41989  limsupubuzlem  42000  xlimmnfvlem2  42121  xlimpnfvlem2  42125  climxlim2lem  42133  dvdivbd  42215  ioodvbdlimc1lem1  42223  dvnprodlem2  42239  iblsplit  42258  stoweidlem5  42297  stoweidlem16  42308  stoweidlem21  42313  stoweidlem24  42316  stoweidlem25  42317  stoweidlem28  42320  stoweidlem31  42323  stoweidlem41  42333  stoweidlem42  42334  stoweidlem44  42336  stoweidlem45  42337  stoweidlem48  42340  stoweidlem51  42343  stoweidlem54  42346  stoweidlem57  42349  stoweidlem60  42352  stoweidlem62  42354  stirlinglem5  42370  dirkercncflem3  42397  fourierdlem11  42410  fourierdlem12  42411  fourierdlem14  42413  fourierdlem15  42414  fourierdlem31  42430  fourierdlem34  42433  fourierdlem41  42440  fourierdlem48  42446  fourierdlem49  42447  fourierdlem50  42448  fourierdlem54  42452  fourierdlem69  42467  fourierdlem73  42471  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem79  42477  fourierdlem80  42478  fourierdlem81  42479  fourierdlem92  42490  fourierdlem93  42491  fourierdlem94  42492  fourierdlem97  42495  fourierdlem103  42501  fourierdlem104  42502  fourierdlem111  42509  fourierdlem113  42511  etransclem32  42558  subsaliuncllem  42647  sge0rpcpnf  42710  caragendifcl  42803  iinhoiicclem  42962  pimdecfgtioc  43000  issmfgtlem  43039