Theorem r19.21bi 2916

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2020.)

Hypothesis

Ref	Expression
r19.21bi.1	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Assertion

Ref	Expression
r19.21bi	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Proof of Theorem r19.21bi

Step	Hyp	Ref	Expression
1		r19.21bi.1	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
2		rsp 2913	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	3	imp 444	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901

This theorem is referenced by:  r19.21be  2917  rspec2  2918  rspec3  2919  ralxfr2d  4808  f1oresrab  6302  isoselem  6491  boxcutc  7837  xpf1o  8007  fineqvlem  8059  indexfi  8157  dffi3  8220  suppr  8260  supiso  8264  infpr  8292  ordtypelem9  8314  brwdom3  8370  xpwdomg  8373  ixpiunwdom  8379  infxpenc2lem1  8725  hsmexlem4  9134  gchina  9400  wunom  9421  prcdnq  9694  prnmax  9696  dedekind  10079  dedekindle  10080  monoord2  12694  seqshft  13673  limsupgre  14060  limsupbnd1  14061  limsupbnd2  14062  climmpt2  14152  rlimcld2  14157  rlimmptrcl  14186  lo1mptrcl  14200  o1mptrcl  14201  climsup  14248  sumpr  14321  sumtp  14322  fsum2dlem  14343  fsumiun  14394  fprod2dlem  14549  iserodd  15378  vdwlem1  15523  vdwlem6  15528  vdwnnlem3  15539  imasvscafn  16020  fuciso  16458  evlfcl  16685  yonedainv  16744  acsmapd  17001  prdsmndd  17146  psgnunilem5  17737  gsummpt1n0  18187  dprdspan  18249  ablfaclem2  18308  srgi  18334  srgrz  18349  srglz  18350  issrngd  18684  psrbaglesupp  19189  psrbagcon  19192  psrass1lem  19198  evlslem2  19333  mpfind  19357  gsumsmonply1  19494  gsummoncoe1  19495  evl1gsummon  19550  frgpcyg  19741  frlmgsum  19930  uvcresum  19951  cpmatmcllem  20342  neiptoptop  20745  neiptopnei  20746  ordtrest2lem  20817  cncmp  21005  1stckgenlem  21166  ptcld  21226  dfac14  21231  txcnp  21233  ptcnplem  21234  ptcnp  21235  ptcn  21240  pthaus  21251  xkococnlem  21272  xkococn  21273  cnmpt11  21276  cnmpt1t  21278  cnmpt12  21280  cnmptkp  21293  cnmptk1  21294  cnmptkk  21296  cnmptk1p  21298  cnmptk2  21299  cnmpt2k  21301  xpstopnlem1  21422  cnpflfi  21613  ptcmplem2  21667  cnextcn  21681  cnextfres1  21682  cnmpt1plusg  21701  cnmpt2plusg  21702  cnmpt1vsca  21807  cnmpt2vsca  21808  ustfilxp  21826  utoptop  21848  restutop  21851  restutopopn  21852  ucncn  21899  cfilufg  21907  trcfilu  21908  psmet0  21923  psmettri2  21924  prdsxmetlem  21983  prdsbl  22106  prdsxmslem2  22144  psmetutop  22182  cnmpt1ds  22453  cnmpt2ds  22454  cncfmpt2ss  22526  bndth  22565  cnmpt1ip  22854  cnmpt2ip  22855  iscmet3lem2  22898  cmetcusp1  22957  rrxcph  22988  ovoliunlem1  23077  ovoliunlem3  23079  ovoliun  23080  ovoliun2  23081  ovolscalem1  23088  volfiniun  23122  uniioombllem4  23160  mbfmptcl  23210  mbfeqalem  23215  mbfres2  23218  ismbf3d  23227  mbfsup  23237  mbfinf  23238  mbflim  23241  itg1ge0  23259  itg1mulc  23277  i1fposd  23280  itg1climres  23287  mbfi1fseqlem4  23291  itg2lea  23317  itg2splitlem  23321  itg2split  23322  itg2monolem1  23323  itg2mono  23326  itg2i1fseqle  23327  itg2i1fseq  23328  itg2addlem  23331  itg2cnlem1  23334  itgeqa  23386  itgss3  23387  itgfsum  23399  itgabs  23407  itggt0  23414  dvmptcl  23528  dvmptco  23541  dvlipcn  23561  dvle  23574  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  dvmptrecl  23591  dvfsumlem2  23594  itgparts  23614  itgsubstlem  23615  itgsubst  23616  coeeulem  23784  dgrlem  23789  dgrlb  23796  coeaddlem  23809  coecj  23838  ulmss  23955  ulmdvlem2  23959  itgulm2  23967  logtayl  24206  leibpi  24469  xrlimcnp  24495  o1cxp  24501  jensen  24515  lgambdd  24563  wilthlem2  24595  sqff1o  24708  fsumdvdscom  24711  fsumdvdsmul  24721  dchrmulcl  24774  dchrmulid2  24777  dchrinv  24786  dchrisumlem3  24980  dchrvmasumlem2  24987  ostth1  25122  ercgrg  25212  f1otrg  25551  f1otrge  25552  ubthlem2  27111  fmptcof2  28839  disjdsct  28863  ressprs  28986  oduprs  28987  archiabl  29083  lmodslmd  29088  txomap  29229  qtophaus  29231  locfinreflem  29235  ordtrest2NEWlem  29296  lmdvg  29327  esumcl  29419  esumeq2d  29426  esumnul  29437  hasheuni  29474  esumcvg  29475  esumcvgre  29480  insiga  29527  ldsysgenld  29550  ldgenpisyslem1  29553  measvunilem  29602  measvunilem0  29603  measdivcstOLD  29614  cntmeas  29616  voliune  29619  volfiniune  29620  1stmbfm  29649  2ndmbfm  29650  omssubadd  29689  difelcarsg  29699  inelcarsg  29700  eulerpartlems  29749  eulerpartlemsv3  29750  eulerpartlemgvv  29765  dstrvprob  29860  bnj93  30187  bnj518  30210  bnj1489  30378  subfacp1lem3  30418  subfacp1lem5  30420  erdszelem8  30434  ptpcon  30469  rescon  30482  cvmliftmolem2  30518  cvmlift2lem11  30549  cvmliftphtlem  30553  mclsax  30720  fin2so  32566  poimirlem18  32597  poimirlem21  32600  mblfinlem2  32617  itgabsnc  32649  itggt0cn  32652  prdsbnd  32762  prdstotbnd  32763  prdsbnd2  32764  rrnequiv  32804  eqlkr3  33406  dih1dimatlem  35636  fnwe2lem1  36638  imo72b2  37497  rfcnnnub  38218  disjxp1  38263  mptex2  38344  fompt  38374  dmrelrnrel  38414  fvmptelrn  38423  suplesup  38496  infxr  38524  climinf  38673  climsuse  38675  mullimc  38683  limccog  38687  mullimcf  38690  limcperiod  38695  limcleqr  38711  neglimc  38714  0ellimcdiv  38716  limclner  38718  dvdivbd  38813  ioodvbdlimc1lem1  38821  dvnprodlem2  38837  iblsplit  38858  stoweidlem5  38898  stoweidlem16  38909  stoweidlem21  38914  stoweidlem24  38917  stoweidlem25  38918  stoweidlem28  38921  stoweidlem31  38924  stoweidlem41  38934  stoweidlem42  38935  stoweidlem44  38937  stoweidlem45  38938  stoweidlem48  38941  stoweidlem51  38944  stoweidlem54  38947  stoweidlem57  38950  stoweidlem60  38953  stoweidlem62  38955  stirlinglem5  38971  dirkercncflem3  38998  fourierdlem11  39011  fourierdlem12  39012  fourierdlem14  39014  fourierdlem15  39015  fourierdlem31  39031  fourierdlem34  39034  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem54  39053  fourierdlem69  39068  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem79  39078  fourierdlem80  39079  fourierdlem81  39080  fourierdlem92  39091  fourierdlem93  39092  fourierdlem94  39093  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem113  39112  etransclem32  39159  subsaliuncllem  39251  sge0rpcpnf  39314  caragendifcl  39404  iinhoiicclem  39564  pimdecfgtioc  39602  issmfgtlem  39642