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 592	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3077

This theorem is used by:  r19.21be  3255  rspec2  3281  rspec3  3282  ralxfr2d  5375  fvmptelcdm  7107  fompt  7112  f1oresrab  7122  isoselem  7343  mpoexw  8078  naddsuc2  8691  boxcutc  8949  xpf1o  9138  fineqvlem  9237  indexfi  9328  dffi3  9402  suppr  9443  supiso  9447  infpr  9476  ordtypelem9  9499  brwdom3  9555  xpwdomg  9558  ixpiunwdom  9563  infxpenc2lem1  10023  hsmexlem4  10432  gchina  10709  wunom  10730  prcdnq  11003  prnmax  11005  dedekind  11398  dedekindle  11399  monoord2  14098  ccatf1  14657  limsupgre  15569  limsupbnd1  15570  limsupbnd2  15571  climmpt2  15661  rlimcld2  15666  climsup  15758  sumpr  15835  sumtp  15836  fsum2dlem  15857  fsumiun  15909  fprod2dlem  16068  iserodd  16928  vdwlem1  17074  vdwlem6  17079  vdwnnlem3  17090  imasvscafn  17624  fuciso  18068  evlfcl  18311  yonedainv  18370  oduprs  18389  acsmapd  18643  chnccats1  18714  chnccat  18715  prdsmndd  18878  psgnunilem5  19622  gsummpt1n0  20093  dprdspan  20157  ablfaclem2  20216  srgdilem  20332  srgrz  20347  srglz  20348  issrngd  21022  frgpcyg  21787  psrbaglesupp  22138  psrbagcon  22141  psrbagleadd1  22144  evlslem2  22296  mpfind  22332  psdmul  22395  ply1chr  22532  gsumsmonply1  22533  gsummoncoe1  22534  evl1gsummon  22591  cpmatmcllem  22944  neiptoptop  23357  neiptopnei  23358  ordtrest2lem  23429  cncmp  23618  1stckgenlem  23780  ptcld  23840  dfac14  23845  ptcnplem  23848  pthaus  23865  xkococnlem  23886  xkococn  23887  cnmpt2k  23915  xpstopnlem1  24036  cnpflfi  24226  ptcmplem2  24280  cnextcn  24294  cnextfres1  24295  cnmpt2plusg  24315  cnmpt2vsca  24422  ustfilxp  24440  utoptop  24461  restutop  24464  restutopopn  24465  ucncn  24511  cfilufg  24519  trcfilu  24520  psmet0  24535  psmettri2  24536  prdsxmetlem  24595  prdsbl  24718  prdsxmslem2  24756  psmetutop  24794  cnmpt2ds  25071  bndth  25187  cnmpt2ip  25477  iscmet3lem2  25521  cmetcusp1  25582  rrxcph  25621  ovoliunlem1  25731  ovoliunlem3  25733  ovoliun  25734  ovoliun2  25735  ovolscalem1  25742  volfiniun  25776  uniioombllem4  25815  mbfeqalem1  25870  mbfres2  25874  ismbf3d  25883  mbfsup  25893  mbfinf  25894  mbflim  25897  itg1ge0  25915  itg1mulc  25933  itg1climres  25943  mbfi1fseqlem4  25947  itg2lea  25973  itg2splitlem  25977  itg2split  25978  itg2monolem1  25979  itg2mono  25982  itg2i1fseqle  25983  itg2i1fseq  25984  itg2addlem  25987  itg2cnlem1  25990  itgeqa  26042  itgfsum  26055  itgabs  26063  itggt0  26072  dvlipcn  26222  dvfsumabs  26251  dvfsumlem2  26255  itgsubstlem  26276  coeeulem  26451  dgrlem  26456  dgrlb  26463  coeaddlem  26476  coecj  26505  coecjOLD  26507  ulmss  26634  leibpi  27180  xrlimcnp  27206  o1cxp  27212  jensen  27226  lgambdd  27274  wilthlem2  27306  sqff1o  27419  fsumdvdscom  27422  fsumdvdsmul  27432  dchrmulcl  27486  dchrmullid  27489  dchrinv  27498  dchrvmasumlem2  27735  ostth1  27870  conway  28045  lesrec  28065  ercgrg  28860  f1otrg  29328  f1otrge  29329  ubthlem2  31353  fmptcof2  33131  disjdsct  33176  fprodex01  33296  prodindf  33309  ressprs  33407  mgcf1o  33444  gsumpart  33504  suppgsumssiun  33513  archiabl  33639  lmodslmd  33645  elrgspnlem1  33683  elrgspnlem2  33684  elrgspnsubrunlem2  33689  rhmimaidl  33861  gsummoncoe1fzo  34008  ply1gsumz  34010  vietadeg1  34089  vietalem  34090  fedgmullem2  34141  fedgmul  34142  txomap  34345  qtophaus  34347  locfinreflem  34351  ordtrest2NEWlem  34433  lmdvg  34464  zrhcntr  34490  esumcl  34541  esumeq2d  34548  esumnul  34559  hasheuni  34596  esumcvg  34597  esumcvgre  34602  insiga  34649  ldsysgenld  34672  ldgenpisyslem1  34675  measvunilem  34724  measvunilem0  34725  measdivcstALTV  34737  cntmeas  34738  voliune  34741  volfiniune  34742  1stmbfm  34772  2ndmbfm  34773  omssubadd  34812  difelcarsg  34822  inelcarsg  34823  eulerpartlems  34872  eulerpartlemsv3  34873  eulerpartlemgvv  34888  dstrvprob  34984  hashreprin  35129  reprgt  35130  breprexplemc  35141  circlemeth  35149  hgt750lema  35166  tgoldbachgtd  35171  bnj93  35373  bnj518  35396  bnj1489  35566  fnrelpredd  35597  subfacp1lem3  35762  subfacp1lem5  35764  erdszelem8  35778  ptpconn  35813  resconn  35826  cvmliftmolem2  35862  cvmlift2lem11  35893  cvmliftphtlem  35897  mclsax  36149  weiunfr  37087  fin2so  38362  poimirlem18  38388  poimirlem21  38391  mblfinlem2  38408  itgabsnc  38439  itggt0cn  38440  prdsbnd  38544  prdstotbnd  38545  prdsbnd2  38546  rrnequiv  38586  eqlkr3  39975  dih1dimatlem  42203  3factsumint  42892  aks6d1c5lem2  43005  fnwe2lem1  43892  cantnf2  44167  nadd1suc  44234  imo72b2  45013  rfcnnnub  45871  disjxp1  45904  disjinfi  46025  fvixp2  46031  dmrelrnrel  46057  fvmptelcdmf  46100  suplesup  46170  infxr  46197  monoord2xrv  46312  climinf  46437  climsuse  46439  mullimc  46447  limccog  46451  mullimcf  46454  limcperiod  46459  limcleqr  46473  neglimc  46476  0ellimcdiv  46478  limclner  46480  limsuppnfdlem  46530  limsupubuzlem  46541  xlimmnfvlem2  46662  xlimpnfvlem2  46666  climxlim2lem  46674  dvdivbd  46752  ioodvbdlimc1lem1  46760  dvnprodlem2  46776  iblsplit  46795  stoweidlem5  46834  stoweidlem16  46845  stoweidlem21  46850  stoweidlem24  46853  stoweidlem25  46854  stoweidlem28  46857  stoweidlem31  46860  stoweidlem41  46870  stoweidlem42  46871  stoweidlem44  46873  stoweidlem45  46874  stoweidlem48  46877  stoweidlem51  46880  stoweidlem54  46883  stoweidlem57  46886  stoweidlem60  46889  stoweidlem62  46891  stirlinglem5  46907  dirkercncflem3  46934  fourierdlem11  46947  fourierdlem12  46948  fourierdlem14  46950  fourierdlem15  46951  fourierdlem31  46967  fourierdlem34  46970  fourierdlem41  46977  fourierdlem48  46983  fourierdlem49  46984  fourierdlem50  46985  fourierdlem54  46989  fourierdlem69  47004  fourierdlem73  47008  fourierdlem74  47009  fourierdlem75  47010  fourierdlem76  47011  fourierdlem79  47014  fourierdlem80  47015  fourierdlem81  47016  fourierdlem92  47027  fourierdlem93  47028  fourierdlem94  47029  fourierdlem97  47032  fourierdlem103  47038  fourierdlem104  47039  fourierdlem111  47046  fourierdlem113  47048  etransclem32  47095  subsaliuncllem  47186  sge0rpcpnf  47250  caragendifcl  47343  iinhoiicclem  47502  pimdecfgtioc  47544  issmfgtlem  47584  ormklocald  47705  ormkglobd  47706  chnrin  47725  tmachlem-agreesn  47776  initopropd  50170  termopropd  50171  thincciso2  50382