Theorem r19.21bi 3229

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

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

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 3052

This theorem is referenced by:  r19.21be  3230  rspec2  3256  rspec3  3257  ralxfr2d  5352  fvmptelcdm  7065  fompt  7070  f1oresrab  7080  isoselem  7296  mpoexw  8031  naddsuc2  8637  boxcutc  8889  xpf1o  9077  fineqvlem  9176  indexfi  9270  dffi3  9344  suppr  9385  supiso  9389  infpr  9418  ordtypelem9  9441  brwdom3  9497  xpwdomg  9500  ixpiunwdom  9505  infxpenc2lem1  9941  hsmexlem4  10351  gchina  10622  wunom  10643  prcdnq  10916  prnmax  10918  dedekind  11309  dedekindle  11310  monoord2  13995  limsupgre  15443  limsupbnd1  15444  limsupbnd2  15445  climmpt2  15535  rlimcld2  15540  climsup  15632  sumpr  15710  sumtp  15711  fsum2dlem  15732  fsumiun  15784  fprod2dlem  15945  iserodd  16806  vdwlem1  16952  vdwlem6  16957  vdwnnlem3  16968  imasvscafn  17501  fuciso  17945  evlfcl  18188  yonedainv  18247  oduprs  18266  acsmapd  18520  chnccats1  18591  chnccat  18592  prdsmndd  18738  psgnunilem5  19469  gsummpt1n0  19940  dprdspan  20004  ablfaclem2  20063  srgdilem  20173  srgrz  20188  srglz  20189  issrngd  20832  frgpcyg  21553  psrbaglesupp  21902  psrbagcon  21905  psrbagleadd1  21908  evlslem2  22057  mpfind  22093  psdmul  22132  ply1chr  22271  gsumsmonply1  22272  gsummoncoe1  22273  evl1gsummon  22330  cpmatmcllem  22683  neiptoptop  23096  neiptopnei  23097  ordtrest2lem  23168  cncmp  23357  1stckgenlem  23518  ptcld  23578  dfac14  23583  ptcnplem  23586  pthaus  23603  xkococnlem  23624  xkococn  23625  cnmpt2k  23653  xpstopnlem1  23774  cnpflfi  23964  ptcmplem2  24018  cnextcn  24032  cnextfres1  24033  cnmpt2plusg  24053  cnmpt2vsca  24160  ustfilxp  24178  utoptop  24199  restutop  24202  restutopopn  24203  ucncn  24249  cfilufg  24257  trcfilu  24258  psmet0  24273  psmettri2  24274  prdsxmetlem  24333  prdsbl  24456  prdsxmslem2  24494  psmetutop  24532  cnmpt2ds  24809  bndth  24925  cnmpt2ip  25215  iscmet3lem2  25259  cmetcusp1  25320  rrxcph  25359  ovoliunlem1  25469  ovoliunlem3  25471  ovoliun  25472  ovoliun2  25473  ovolscalem1  25480  volfiniun  25514  uniioombllem4  25553  mbfeqalem1  25608  mbfres2  25612  ismbf3d  25621  mbfsup  25631  mbfinf  25632  mbflim  25635  itg1ge0  25653  itg1mulc  25671  itg1climres  25681  mbfi1fseqlem4  25685  itg2lea  25711  itg2splitlem  25715  itg2split  25716  itg2monolem1  25717  itg2mono  25720  itg2i1fseqle  25721  itg2i1fseq  25722  itg2addlem  25725  itg2cnlem1  25728  itgeqa  25781  itgfsum  25794  itgabs  25802  itggt0  25811  dvlipcn  25961  dvfsumabs  25990  dvfsumlem2  25994  itgsubstlem  26015  coeeulem  26189  dgrlem  26194  dgrlb  26201  coeaddlem  26214  coecj  26243  coecjOLD  26245  ulmss  26362  leibpi  26906  xrlimcnp  26932  o1cxp  26938  jensen  26952  lgambdd  27000  wilthlem2  27032  sqff1o  27145  fsumdvdscom  27148  fsumdvdsmul  27158  dchrmulcl  27212  dchrmullid  27215  dchrinv  27224  dchrvmasumlem2  27461  ostth1  27596  conway  27771  lesrec  27791  ercgrg  28585  f1otrg  28939  f1otrge  28940  ubthlem2  30942  fmptcof2  32730  disjdsct  32776  fprodex01  32898  prodindf  32922  ccatf1  33009  ressprs  33026  mgcf1o  33063  gsumpart  33124  suppgsumssiun  33133  archiabl  33259  lmodslmd  33265  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnsubrunlem2  33309  rhmimaidl  33492  gsummoncoe1fzo  33657  ply1gsumz  33659  vietadeg1  33722  vietalem  33723  fedgmullem2  33774  fedgmul  33775  txomap  33978  qtophaus  33980  locfinreflem  33984  ordtrest2NEWlem  34066  lmdvg  34097  zrhcntr  34123  esumcl  34174  esumeq2d  34181  esumnul  34192  hasheuni  34229  esumcvg  34230  esumcvgre  34235  insiga  34281  ldsysgenld  34304  ldgenpisyslem1  34307  measvunilem  34356  measvunilem0  34357  measdivcstALTV  34369  cntmeas  34370  voliune  34373  volfiniune  34374  1stmbfm  34404  2ndmbfm  34405  omssubadd  34444  difelcarsg  34454  inelcarsg  34455  eulerpartlems  34504  eulerpartlemsv3  34505  eulerpartlemgvv  34520  dstrvprob  34616  hashreprin  34764  reprgt  34765  breprexplemc  34776  circlemeth  34784  hgt750lema  34801  tgoldbachgtd  34806  bnj93  35005  bnj518  35028  bnj1489  35198  fnrelpredd  35234  subfacp1lem3  35364  subfacp1lem5  35366  erdszelem8  35380  ptpconn  35415  resconn  35428  cvmliftmolem2  35464  cvmlift2lem11  35495  cvmliftphtlem  35499  mclsax  35751  weiunfr  36649  fin2so  37928  poimirlem18  37959  poimirlem21  37962  mblfinlem2  37979  itgabsnc  38010  itggt0cn  38011  prdsbnd  38114  prdstotbnd  38115  prdsbnd2  38116  rrnequiv  38156  eqlkr3  39547  dih1dimatlem  41775  3factsumint  42464  aks6d1c5lem2  42577  fnwe2lem1  43478  cantnf2  43753  nadd1suc  43820  imo72b2  44599  rfcnnnub  45467  disjxp1  45500  disjinfi  45622  fvixp2  45628  dmrelrnrel  45655  fvmptelcdmf  45699  suplesup  45769  infxr  45796  monoord2xrv  45911  climinf  46036  climsuse  46038  mullimc  46046  limccog  46050  mullimcf  46053  limcperiod  46058  limcleqr  46072  neglimc  46075  0ellimcdiv  46077  limclner  46079  limsuppnfdlem  46129  limsupubuzlem  46140  xlimmnfvlem2  46261  xlimpnfvlem2  46265  climxlim2lem  46273  dvdivbd  46351  ioodvbdlimc1lem1  46359  dvnprodlem2  46375  iblsplit  46394  stoweidlem5  46433  stoweidlem16  46444  stoweidlem21  46449  stoweidlem24  46452  stoweidlem25  46453  stoweidlem28  46456  stoweidlem31  46459  stoweidlem41  46469  stoweidlem42  46470  stoweidlem44  46472  stoweidlem45  46473  stoweidlem48  46476  stoweidlem51  46479  stoweidlem54  46482  stoweidlem57  46485  stoweidlem60  46488  stoweidlem62  46490  stirlinglem5  46506  dirkercncflem3  46533  fourierdlem11  46546  fourierdlem12  46547  fourierdlem14  46549  fourierdlem15  46550  fourierdlem31  46566  fourierdlem34  46569  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem54  46588  fourierdlem69  46603  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem79  46613  fourierdlem80  46614  fourierdlem81  46615  fourierdlem92  46626  fourierdlem93  46627  fourierdlem94  46628  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem113  46647  etransclem32  46694  subsaliuncllem  46785  sge0rpcpnf  46849  caragendifcl  46942  iinhoiicclem  47101  pimdecfgtioc  47143  issmfgtlem  47183  ormklocald  47304  ormkglobd  47305  initopropd  49718  termopropd  49719  thincciso2  49930