Theorem r19.21bi 3227

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045

This theorem is referenced by:  r19.21be  3228  rspec2  3254  rspec3  3255  ralxfr2d  5360  fvmptelcdm  7067  fompt  7072  f1oresrab  7081  isoselem  7298  mpoexw  8036  naddsuc2  8642  boxcutc  8891  xpf1o  9080  fineqvlem  9185  indexfi  9287  dffi3  9358  suppr  9399  supiso  9403  infpr  9432  ordtypelem9  9455  brwdom3  9511  xpwdomg  9514  ixpiunwdom  9519  infxpenc2lem1  9948  hsmexlem4  10358  gchina  10628  wunom  10649  prcdnq  10922  prnmax  10924  dedekind  11313  dedekindle  11314  monoord2  13974  limsupgre  15423  limsupbnd1  15424  limsupbnd2  15425  climmpt2  15515  rlimcld2  15520  climsup  15612  sumpr  15690  sumtp  15691  fsum2dlem  15712  fsumiun  15763  fprod2dlem  15922  iserodd  16782  vdwlem1  16928  vdwlem6  16933  vdwnnlem3  16944  imasvscafn  17476  fuciso  17920  evlfcl  18163  yonedainv  18222  oduprs  18241  acsmapd  18495  prdsmndd  18679  psgnunilem5  19408  gsummpt1n0  19879  dprdspan  19943  ablfaclem2  20002  srgdilem  20112  srgrz  20127  srglz  20128  issrngd  20775  frgpcyg  21515  psrbaglesupp  21864  psrbagcon  21867  psrbagleadd1  21870  evlslem2  22019  mpfind  22047  psdmul  22086  ply1chr  22226  gsumsmonply1  22227  gsummoncoe1  22228  evl1gsummon  22285  cpmatmcllem  22638  neiptoptop  23051  neiptopnei  23052  ordtrest2lem  23123  cncmp  23312  1stckgenlem  23473  ptcld  23533  dfac14  23538  ptcnplem  23541  pthaus  23558  xkococnlem  23579  xkococn  23580  cnmpt2k  23608  xpstopnlem1  23729  cnpflfi  23919  ptcmplem2  23973  cnextcn  23987  cnextfres1  23988  cnmpt2plusg  24008  cnmpt2vsca  24115  ustfilxp  24133  utoptop  24155  restutop  24158  restutopopn  24159  ucncn  24205  cfilufg  24213  trcfilu  24214  psmet0  24229  psmettri2  24230  prdsxmetlem  24289  prdsbl  24412  prdsxmslem2  24450  psmetutop  24488  cnmpt2ds  24765  bndth  24890  cnmpt2ip  25181  iscmet3lem2  25225  cmetcusp1  25286  rrxcph  25325  ovoliunlem1  25436  ovoliunlem3  25438  ovoliun  25439  ovoliun2  25440  ovolscalem1  25447  volfiniun  25481  uniioombllem4  25520  mbfeqalem1  25575  mbfres2  25579  ismbf3d  25588  mbfsup  25598  mbfinf  25599  mbflim  25602  itg1ge0  25620  itg1mulc  25638  itg1climres  25648  mbfi1fseqlem4  25652  itg2lea  25678  itg2splitlem  25682  itg2split  25683  itg2monolem1  25684  itg2mono  25687  itg2i1fseqle  25688  itg2i1fseq  25689  itg2addlem  25692  itg2cnlem1  25695  itgeqa  25748  itgfsum  25761  itgabs  25769  itggt0  25778  dvlipcn  25932  dvfsumabs  25962  dvfsumlem2  25966  dvfsumlem2OLD  25967  itgsubstlem  25988  coeeulem  26162  dgrlem  26167  dgrlb  26174  coeaddlem  26187  coecj  26217  coecjOLD  26219  ulmss  26339  leibpi  26885  xrlimcnp  26911  o1cxp  26918  jensen  26932  lgambdd  26980  wilthlem2  27012  sqff1o  27125  fsumdvdscom  27128  fsumdvdsmul  27138  fsumdvdsmulOLD  27140  dchrmulcl  27193  dchrmullid  27196  dchrinv  27205  dchrvmasumlem2  27442  ostth1  27577  conway  27745  slerec  27765  ercgrg  28497  f1otrg  28851  f1otrge  28852  ubthlem2  30850  fmptcof2  32631  disjdsct  32676  fprodex01  32800  prodindf  32836  ccatf1  32920  ressprs  32938  mgcf1o  32975  chnccats1  32987  gsumpart  33040  archiabl  33167  lmodslmd  33173  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnsubrunlem2  33215  rhmimaidl  33396  gsummoncoe1fzo  33556  ply1gsumz  33557  fedgmullem2  33619  fedgmul  33620  txomap  33817  qtophaus  33819  locfinreflem  33823  ordtrest2NEWlem  33905  lmdvg  33936  zrhcntr  33962  esumcl  34013  esumeq2d  34020  esumnul  34031  hasheuni  34068  esumcvg  34069  esumcvgre  34074  insiga  34120  ldsysgenld  34143  ldgenpisyslem1  34146  measvunilem  34195  measvunilem0  34196  measdivcstALTV  34208  cntmeas  34209  voliune  34212  volfiniune  34213  1stmbfm  34244  2ndmbfm  34245  omssubadd  34284  difelcarsg  34294  inelcarsg  34295  eulerpartlems  34344  eulerpartlemsv3  34345  eulerpartlemgvv  34360  dstrvprob  34456  hashreprin  34604  reprgt  34605  breprexplemc  34616  circlemeth  34624  hgt750lema  34641  tgoldbachgtd  34646  bnj93  34846  bnj518  34869  bnj1489  35039  fnrelpredd  35072  subfacp1lem3  35162  subfacp1lem5  35164  erdszelem8  35178  ptpconn  35213  resconn  35226  cvmliftmolem2  35262  cvmlift2lem11  35293  cvmliftphtlem  35297  mclsax  35549  weiunfr  36448  fin2so  37594  poimirlem18  37625  poimirlem21  37628  mblfinlem2  37645  itgabsnc  37676  itggt0cn  37677  prdsbnd  37780  prdstotbnd  37781  prdsbnd2  37782  rrnequiv  37822  eqlkr3  39087  dih1dimatlem  41316  3factsumint  42006  aks6d1c5lem2  42119  fnwe2lem1  43032  cantnf2  43307  nadd1suc  43374  imo72b2  44154  rfcnnnub  45023  disjxp1  45056  disjinfi  45179  fvixp2  45186  dmrelrnrel  45213  fvmptelcdmf  45257  suplesup  45328  infxr  45356  monoord2xrv  45472  climinf  45597  climsuse  45599  mullimc  45607  limccog  45611  mullimcf  45614  limcperiod  45619  limcleqr  45635  neglimc  45638  0ellimcdiv  45640  limclner  45642  limsuppnfdlem  45692  limsupubuzlem  45703  xlimmnfvlem2  45824  xlimpnfvlem2  45828  climxlim2lem  45836  dvdivbd  45914  ioodvbdlimc1lem1  45922  dvnprodlem2  45938  iblsplit  45957  stoweidlem5  45996  stoweidlem16  46007  stoweidlem21  46012  stoweidlem24  46015  stoweidlem25  46016  stoweidlem28  46019  stoweidlem31  46022  stoweidlem41  46032  stoweidlem42  46033  stoweidlem44  46035  stoweidlem45  46036  stoweidlem48  46039  stoweidlem51  46042  stoweidlem54  46045  stoweidlem57  46048  stoweidlem60  46051  stoweidlem62  46053  stirlinglem5  46069  dirkercncflem3  46096  fourierdlem11  46109  fourierdlem12  46110  fourierdlem14  46112  fourierdlem15  46113  fourierdlem31  46129  fourierdlem34  46132  fourierdlem41  46139  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem54  46151  fourierdlem69  46166  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem79  46176  fourierdlem80  46177  fourierdlem81  46178  fourierdlem92  46189  fourierdlem93  46190  fourierdlem94  46191  fourierdlem97  46194  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  fourierdlem113  46210  etransclem32  46257  subsaliuncllem  46348  sge0rpcpnf  46412  caragendifcl  46505  iinhoiicclem  46664  pimdecfgtioc  46706  issmfgtlem  46746  ormklocald  46865  ormkglobd  46866  initopropd  49225  termopropd  49226  thincciso2  49437