Theorem r19.21bi 3258

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

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

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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  r19.21be  3259  rspec2  3285  rspec3  3286  ralxfr2d  5379  fvmptelcdm  7145  fompt  7150  f1oresrab  7160  isoselem  7380  mpoexw  8126  fnwe2lem2  8183  naddsuc2  8749  boxcutc  9007  xpf1o  9196  fineqvlem  9295  indexfi  9387  dffi3  9460  suppr  9501  supiso  9505  infpr  9534  ordtypelem9  9557  brwdom3  9613  xpwdomg  9616  ixpiunwdom  9621  infxpenc2lem1  10137  hsmexlem4  10546  gchina  10823  wunom  10844  prcdnq  11117  prnmax  11119  dedekind  11512  dedekindle  11513  monoord2  14216  ccatf1  14777  limsupgre  15692  limsupbnd1  15693  limsupbnd2  15694  climmpt2  15784  rlimcld2  15789  climsup  15881  sumpr  15958  sumtp  15959  fsum2dlem  15980  fsumiun  16032  fprod2dlem  16191  iserodd  17057  vdwlem1  17203  vdwlem6  17208  vdwnnlem3  17219  imasvscafn  17759  fuciso  18203  evlfcl  18446  yonedainv  18505  oduprs  18524  acsmapd  18778  chnccats1  18849  chnccat  18850  prdsmndd  19014  psgnunilem5  19759  gsummpt1n0  20230  dprdspan  20294  ablfaclem2  20353  srgdilem  20469  srgrz  20484  srglz  20485  issrngd  21163  frgpcyg  21934  psrbaglesupp  22285  psrbagcon  22288  psrbagleadd1  22291  evlslem2  22443  mpfind  22479  psdmul  22542  ply1chr  22679  gsumsmonply1  22680  gsummoncoe1  22681  evl1gsummon  22738  cpmatmcllem  23091  neiptoptop  23504  neiptopnei  23505  ordtrest2lem  23576  cncmp  23765  1stckgenlem  23927  ptcld  23987  dfac14  23992  ptcnplem  23995  pthaus  24012  xkococnlem  24033  xkococn  24034  cnmpt2k  24062  xpstopnlem1  24183  cnpflfi  24373  ptcmplem2  24427  cnextcn  24441  cnextfres1  24442  cnmpt2plusg  24462  cnmpt2vsca  24569  ustfilxp  24587  utoptop  24608  restutop  24611  restutopopn  24612  ucncn  24658  cfilufg  24666  trcfilu  24667  psmet0  24682  psmettri2  24683  prdsxmetlem  24742  prdsbl  24865  prdsxmslem2  24903  psmetutop  24941  cnmpt2ds  25218  bndth  25334  cnmpt2ip  25624  iscmet3lem2  25668  cmetcusp1  25729  rrxcph  25768  ovoliunlem1  25878  ovoliunlem3  25880  ovoliun  25881  ovoliun2  25882  ovolscalem1  25889  volfiniun  25923  uniioombllem4  25962  mbfeqalem1  26017  mbfres2  26021  ismbf3d  26030  mbfsup  26040  mbfinf  26041  mbflim  26044  itg1ge0  26062  itg1mulc  26080  itg1climres  26090  mbfi1fseqlem4  26094  itg2lea  26120  itg2splitlem  26124  itg2split  26125  itg2monolem1  26126  itg2mono  26129  itg2i1fseqle  26130  itg2i1fseq  26131  itg2addlem  26134  itg2cnlem1  26137  itgeqa  26189  itgfsum  26202  itgabs  26210  itggt0  26219  dvlipcn  26369  dvfsumabs  26398  dvfsumlem2  26402  itgsubstlem  26423  coeeulem  26598  dgrlem  26603  dgrlb  26610  coeaddlem  26623  coecj  26652  ulmss  26781  leibpi  27327  xrlimcnp  27353  o1cxp  27359  jensen  27373  lgambdd  27421  wilthlem2  27453  sqff1o  27566  fsumdvdscom  27569  fsumdvdsmul  27579  dchrmulcl  27633  dchrmullid  27636  dchrinv  27645  dchrvmasumlem2  27882  ostth1  28017  conway  28222  lesrec  28242  ercgrg  29037  f1otrg  29505  f1otrge  29506  ubthlem2  31530  fmptcof2  33349  disjdsct  33393  fprodex01  33512  prodindf  33525  ressprs  33623  weinfcl  33636  mgcf1o  33663  gsumpart  33723  suppgsumssiun  33732  archiabl  33858  lmodslmd  33864  elrgspnlem1  33902  elrgspnlem2  33903  elrgspnsubrunlem2  33908  rhmimaidl  34086  gsummoncoe1fzo  34232  ply1gsumz  34234  vietadeg1  34321  vietalem  34322  fedgmullem2  34373  fedgmul  34374  txomap  34577  qtophaus  34579  locfinreflem  34583  ordtrest2NEWlem  34665  lmdvg  34696  zrhcntr  34722  esumcl  34773  esumeq2d  34780  esumnul  34791  hasheuni  34828  esumcvg  34829  esumcvgre  34834  insiga  34881  ldsysgenld  34904  ldgenpisyslem1  34907  measvunilem  34956  measvunilem0  34957  measdivcstALTV  34969  cntmeas  34970  voliune  34973  volfiniune  34974  1stmbfm  35003  2ndmbfm  35004  omssubadd  35043  difelcarsg  35053  inelcarsg  35054  eulerpartlems  35103  eulerpartlemsv3  35104  eulerpartlemgvv  35119  dstrvprob  35215  hashreprin  35360  reprgt  35361  breprexplemc  35372  circlemeth  35380  hgt750lema  35397  tgoldbachgtd  35402  bnj93  35604  bnj518  35627  bnj1489  35797  fnrelpredd  35845  srepdf  36128  subfacp1lem3  36155  subfacp1lem5  36157  erdszelem8  36171  ptpconn  36206  resconn  36219  cvmliftmolem2  36255  cvmlift2lem11  36286  cvmliftphtlem  36290  mclsax  36542  weiunfr  37470  fin2so  38798  poimirlem18  38824  poimirlem21  38827  mblfinlem2  38844  itgabsnc  38875  itggt0cn  38876  prdsbnd  38993  prdstotbnd  38994  prdsbnd2  38995  rrnequiv  39035  eqlkr3  40424  dih1dimatlem  42652  3factsumint  43341  aks6d1c5lem2  43454  cantnf2  44588  nadd1suc  44655  imo72b2  45433  rfcnnnub  46327  disjxp1  46360  disjinfi  46480  fvixp2  46486  dmrelrnrel  46512  fvmptelcdmf  46555  suplesup  46624  infxr  46651  monoord2xrv  46766  climinf  46891  climsuse  46893  mullimc  46901  limccog  46905  mullimcf  46908  limcperiod  46913  limcleqr  46927  neglimc  46930  0ellimcdiv  46932  limclner  46934  limsuppnfdlem  46984  limsupubuzlem  46995  xlimmnfvlem2  47116  xlimpnfvlem2  47120  climxlim2lem  47128  dvdivbd  47206  ioodvbdlimc1lem1  47214  dvnprodlem2  47230  iblsplit  47249  stoweidlem5  47288  stoweidlem16  47299  stoweidlem21  47304  stoweidlem24  47307  stoweidlem25  47308  stoweidlem28  47311  stoweidlem31  47314  stoweidlem41  47324  stoweidlem42  47325  stoweidlem44  47327  stoweidlem45  47328  stoweidlem48  47331  stoweidlem51  47334  stoweidlem54  47337  stoweidlem57  47340  stoweidlem60  47343  stoweidlem62  47345  stirlinglem5  47361  dirkercncflem3  47388  fourierdlem11  47401  fourierdlem12  47402  fourierdlem14  47404  fourierdlem15  47405  fourierdlem31  47421  fourierdlem34  47424  fourierdlem41  47431  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem54  47443  fourierdlem69  47458  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem79  47468  fourierdlem80  47469  fourierdlem81  47470  fourierdlem92  47481  fourierdlem93  47482  fourierdlem94  47483  fourierdlem97  47486  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  fourierdlem113  47502  etransclem32  47549  subsaliuncllem  47640  sge0rpcpnf  47704  caragendifcl  47797  iinhoiicclem  47956  pimdecfgtioc  47998  issmfgtlem  48038  ormklocald  48159  ormkglobd  48160  chnrin  48179  tmachlem-agreesn  48230  initopropd  50696  termopropd  50697  thincciso2  50921