Theorem r19.21bi 3231

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3054

This theorem is referenced by:  r19.21be  3232  rspec2  3258  rspec3  3259  ralxfr2d  5339  fvmptelcdm  7054  fompt  7059  f1oresrab  7069  isoselem  7285  mpoexw  8020  naddsuc2  8627  boxcutc  8879  xpf1o  9067  fineqvlem  9166  indexfi  9260  dffi3  9334  suppr  9375  supiso  9379  infpr  9408  ordtypelem9  9431  brwdom3  9487  xpwdomg  9490  ixpiunwdom  9495  infxpenc2lem1  9932  hsmexlem4  10342  gchina  10613  wunom  10634  prcdnq  10907  prnmax  10909  dedekind  11300  dedekindle  11301  monoord2  13986  limsupgre  15434  limsupbnd1  15435  limsupbnd2  15436  climmpt2  15526  rlimcld2  15531  climsup  15623  sumpr  15701  sumtp  15702  fsum2dlem  15723  fsumiun  15775  fprod2dlem  15936  iserodd  16797  vdwlem1  16943  vdwlem6  16948  vdwnnlem3  16959  imasvscafn  17492  fuciso  17936  evlfcl  18179  yonedainv  18238  oduprs  18257  acsmapd  18511  chnccats1  18582  chnccat  18583  prdsmndd  18729  psgnunilem5  19460  gsummpt1n0  19931  dprdspan  19995  ablfaclem2  20054  srgdilem  20164  srgrz  20179  srglz  20180  issrngd  20827  frgpcyg  21548  psrbaglesupp  21897  psrbagcon  21900  psrbagleadd1  21903  evlslem2  22055  mpfind  22091  psdmul  22154  ply1chr  22292  gsumsmonply1  22293  gsummoncoe1  22294  evl1gsummon  22351  cpmatmcllem  22701  neiptoptop  23114  neiptopnei  23115  ordtrest2lem  23186  cncmp  23375  1stckgenlem  23536  ptcld  23596  dfac14  23601  ptcnplem  23604  pthaus  23621  xkococnlem  23642  xkococn  23643  cnmpt2k  23671  xpstopnlem1  23792  cnpflfi  23982  ptcmplem2  24036  cnextcn  24050  cnextfres1  24051  cnmpt2plusg  24071  cnmpt2vsca  24178  ustfilxp  24196  utoptop  24217  restutop  24220  restutopopn  24221  ucncn  24267  cfilufg  24275  trcfilu  24276  psmet0  24291  psmettri2  24292  prdsxmetlem  24351  prdsbl  24474  prdsxmslem2  24512  psmetutop  24550  cnmpt2ds  24827  bndth  24943  cnmpt2ip  25233  iscmet3lem2  25277  cmetcusp1  25338  rrxcph  25377  ovoliunlem1  25487  ovoliunlem3  25489  ovoliun  25490  ovoliun2  25491  ovolscalem1  25498  volfiniun  25532  uniioombllem4  25571  mbfeqalem1  25626  mbfres2  25630  ismbf3d  25639  mbfsup  25649  mbfinf  25650  mbflim  25653  itg1ge0  25671  itg1mulc  25689  itg1climres  25699  mbfi1fseqlem4  25703  itg2lea  25729  itg2splitlem  25733  itg2split  25734  itg2monolem1  25735  itg2mono  25738  itg2i1fseqle  25739  itg2i1fseq  25740  itg2addlem  25743  itg2cnlem1  25746  itgeqa  25799  itgfsum  25812  itgabs  25820  itggt0  25829  dvlipcn  25979  dvfsumabs  26008  dvfsumlem2  26012  itgsubstlem  26033  coeeulem  26207  dgrlem  26212  dgrlb  26219  coeaddlem  26232  coecj  26261  coecjOLD  26263  ulmss  26380  leibpi  26924  xrlimcnp  26950  o1cxp  26956  jensen  26970  lgambdd  27018  wilthlem2  27050  sqff1o  27163  fsumdvdscom  27166  fsumdvdsmul  27176  dchrmulcl  27230  dchrmullid  27233  dchrinv  27242  dchrvmasumlem2  27479  ostth1  27614  conway  27789  lesrec  27809  ercgrg  28603  f1otrg  28957  f1otrge  28958  ubthlem2  30960  fmptcof2  32749  disjdsct  32795  fprodex01  32917  prodindf  32941  ccatf1  33028  ressprs  33045  mgcf1o  33082  gsumpart  33144  suppgsumssiun  33153  archiabl  33279  lmodslmd  33285  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnsubrunlem2  33329  rhmimaidl  33515  gsummoncoe1fzo  33680  ply1gsumz  33682  vietadeg1  33762  vietalem  33763  fedgmullem2  33814  fedgmul  33815  txomap  34018  qtophaus  34020  locfinreflem  34024  ordtrest2NEWlem  34106  lmdvg  34137  zrhcntr  34163  esumcl  34214  esumeq2d  34221  esumnul  34232  hasheuni  34269  esumcvg  34270  esumcvgre  34275  insiga  34321  ldsysgenld  34344  ldgenpisyslem1  34347  measvunilem  34396  measvunilem0  34397  measdivcstALTV  34409  cntmeas  34410  voliune  34413  volfiniune  34414  1stmbfm  34444  2ndmbfm  34445  omssubadd  34484  difelcarsg  34494  inelcarsg  34495  eulerpartlems  34544  eulerpartlemsv3  34545  eulerpartlemgvv  34560  dstrvprob  34656  hashreprin  34804  reprgt  34805  breprexplemc  34816  circlemeth  34824  hgt750lema  34841  tgoldbachgtd  34846  bnj93  35045  bnj518  35068  bnj1489  35238  fnrelpredd  35272  subfacp1lem3  35410  subfacp1lem5  35412  erdszelem8  35426  ptpconn  35461  resconn  35474  cvmliftmolem2  35510  cvmlift2lem11  35541  cvmliftphtlem  35545  mclsax  35797  weiunfr  36695  fin2so  37974  poimirlem18  38005  poimirlem21  38008  mblfinlem2  38025  itgabsnc  38056  itggt0cn  38057  prdsbnd  38160  prdstotbnd  38161  prdsbnd2  38162  rrnequiv  38202  eqlkr3  39593  dih1dimatlem  41821  3factsumint  42510  aks6d1c5lem2  42623  fnwe2lem1  43495  cantnf2  43770  nadd1suc  43837  imo72b2  44616  rfcnnnub  45484  disjxp1  45517  disjinfi  45639  fvixp2  45645  dmrelrnrel  45671  fvmptelcdmf  45714  suplesup  45784  infxr  45811  monoord2xrv  45926  climinf  46051  climsuse  46053  mullimc  46061  limccog  46065  mullimcf  46068  limcperiod  46073  limcleqr  46087  neglimc  46090  0ellimcdiv  46092  limclner  46094  limsuppnfdlem  46144  limsupubuzlem  46155  xlimmnfvlem2  46276  xlimpnfvlem2  46280  climxlim2lem  46288  dvdivbd  46366  ioodvbdlimc1lem1  46374  dvnprodlem2  46390  iblsplit  46409  stoweidlem5  46448  stoweidlem16  46459  stoweidlem21  46464  stoweidlem24  46467  stoweidlem25  46468  stoweidlem28  46471  stoweidlem31  46474  stoweidlem41  46484  stoweidlem42  46485  stoweidlem44  46487  stoweidlem45  46488  stoweidlem48  46491  stoweidlem51  46494  stoweidlem54  46497  stoweidlem57  46500  stoweidlem60  46503  stoweidlem62  46505  stirlinglem5  46521  dirkercncflem3  46548  fourierdlem11  46561  fourierdlem12  46562  fourierdlem14  46564  fourierdlem15  46565  fourierdlem31  46581  fourierdlem34  46584  fourierdlem41  46591  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem54  46603  fourierdlem69  46618  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem79  46628  fourierdlem80  46629  fourierdlem81  46630  fourierdlem92  46641  fourierdlem93  46642  fourierdlem94  46643  fourierdlem97  46646  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fourierdlem113  46662  etransclem32  46709  subsaliuncllem  46800  sge0rpcpnf  46864  caragendifcl  46957  iinhoiicclem  47116  pimdecfgtioc  47158  issmfgtlem  47198  ormklocald  47319  ormkglobd  47320  initopropd  49733  termopropd  49734  thincciso2  49945