Theorem r19.21bi 3114

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 3111	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	3	imp 397	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107  ∀wral 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-12 2163

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-ral 3095

This theorem is referenced by:  r19.21be  3115  rspec2  3116  rspec3  3117  ralxfr2d  5122  fvmptelrn  6647  f1oresrab  6659  isoselem  6863  boxcutc  8237  xpf1o  8410  fineqvlem  8462  indexfi  8562  dffi3  8625  suppr  8665  supiso  8669  infpr  8697  ordtypelem9  8720  brwdom3  8776  xpwdomg  8779  ixpiunwdom  8785  infxpenc2lem1  9175  hsmexlem4  9586  gchina  9856  wunom  9877  prcdnq  10150  prnmax  10152  dedekind  10539  dedekindle  10540  monoord2  13150  limsupgre  14620  limsupbnd1  14621  limsupbnd2  14622  climmpt2  14712  rlimcld2  14717  climsup  14808  sumpr  14884  sumtp  14885  fsum2dlem  14906  fsumiun  14957  fprod2dlem  15113  iserodd  15944  vdwlem1  16089  vdwlem6  16094  vdwnnlem3  16105  imasvscafn  16583  fuciso  17020  evlfcl  17248  yonedainv  17307  acsmapd  17564  prdsmndd  17709  psgnunilem5  18297  psgnunilem5OLD  18298  gsummpt1n0  18750  dprdspan  18813  ablfaclem2  18872  srgi  18898  srgrz  18913  srglz  18914  issrngd  19253  psrbaglesupp  19765  psrbagcon  19768  psrass1lem  19774  evlslem2  19908  mpfind  19932  gsumsmonply1  20069  gsummoncoe1  20070  evl1gsummon  20125  frgpcyg  20317  frlmgsum  20515  uvcresum  20536  cpmatmcllem  20930  neiptoptop  21343  neiptopnei  21344  ordtrest2lem  21415  cncmp  21604  1stckgenlem  21765  ptcld  21825  dfac14  21830  txcnp  21832  ptcnplem  21833  ptcnp  21834  ptcn  21839  pthaus  21850  xkococnlem  21871  xkococn  21872  cnmpt11  21875  cnmpt1t  21877  cnmpt12  21879  cnmptkp  21892  cnmptk1  21893  cnmptkk  21895  cnmptk1p  21897  cnmptk2  21898  cnmpt2k  21900  xpstopnlem1  22021  cnpflfi  22211  ptcmplem2  22265  cnextcn  22279  cnextfres1  22280  cnmpt1plusg  22299  cnmpt2plusg  22300  cnmpt1vsca  22405  cnmpt2vsca  22406  ustfilxp  22424  utoptop  22446  restutop  22449  restutopopn  22450  ucncn  22497  cfilufg  22505  trcfilu  22506  psmet0  22521  psmettri2  22522  prdsxmetlem  22581  prdsbl  22704  prdsxmslem2  22742  psmetutop  22780  cnmpt1ds  23053  cnmpt2ds  23054  cncfmpt2ss  23126  bndth  23165  cnmpt1ip  23453  cnmpt2ip  23454  iscmet3lem2  23498  cmetcusp1  23559  rrxcph  23598  ovoliunlem1  23706  ovoliunlem3  23708  ovoliun  23709  ovoliun2  23710  ovolscalem1  23717  volfiniun  23751  uniioombllem4  23790  mbfmptcl  23840  mbfeqalem1  23845  mbfres2  23849  ismbf3d  23858  mbfsup  23868  mbfinf  23869  mbflim  23872  itg1ge0  23890  itg1mulc  23908  i1fposd  23911  itg1climres  23918  mbfi1fseqlem4  23922  itg2lea  23948  itg2splitlem  23952  itg2split  23953  itg2monolem1  23954  itg2mono  23957  itg2i1fseqle  23958  itg2i1fseq  23959  itg2addlem  23962  itg2cnlem1  23965  itgeqa  24017  itgss3  24018  itgfsum  24030  itgabs  24038  itggt0  24045  dvmptcl  24159  dvmptco  24172  dvlipcn  24194  dvle  24207  dvfsumle  24221  dvfsumge  24222  dvfsumabs  24223  dvmptrecl  24224  dvfsumlem2  24227  itgparts  24247  itgsubstlem  24248  itgsubst  24249  coeeulem  24417  dgrlem  24422  dgrlb  24429  coeaddlem  24442  coecj  24471  ulmss  24588  ulmdvlem2  24592  logtayl  24843  leibpi  25121  xrlimcnp  25147  o1cxp  25153  jensen  25167  lgambdd  25215  wilthlem2  25247  sqff1o  25360  fsumdvdscom  25363  fsumdvdsmul  25373  dchrmulcl  25426  dchrmulid2  25429  dchrinv  25438  dchrisumlem3  25632  dchrvmasumlem2  25639  ostth1  25774  ercgrg  25868  f1otrg  26220  f1otrge  26221  ubthlem2  28299  fmptcof2  30022  disjdsct  30046  fprodex01  30135  ressprs  30217  oduprs  30218  archiabl  30314  lmodslmd  30319  txomap  30499  qtophaus  30501  locfinreflem  30505  ordtrest2NEWlem  30566  lmdvg  30597  prodindf  30683  esumcl  30690  esumeq2d  30697  esumnul  30708  hasheuni  30745  esumcvg  30746  esumcvgre  30751  insiga  30798  ldsysgenld  30821  ldgenpisyslem1  30824  measvunilem  30873  measvunilem0  30874  measdivcstOLD  30885  cntmeas  30887  voliune  30890  volfiniune  30891  1stmbfm  30920  2ndmbfm  30921  omssubadd  30960  difelcarsg  30970  inelcarsg  30971  eulerpartlems  31020  eulerpartlemsv3  31021  eulerpartlemgvv  31036  dstrvprob  31132  hashreprin  31300  reprgt  31301  breprexplemc  31312  circlemeth  31320  hgt750lema  31337  tgoldbachgtd  31342  bnj93  31532  bnj518  31555  bnj1489  31723  subfacp1lem3  31763  subfacp1lem5  31765  erdszelem8  31779  ptpconn  31814  resconn  31827  cvmliftmolem2  31863  cvmlift2lem11  31894  cvmliftphtlem  31898  mclsax  32065  conway  32499  slerec  32512  fin2so  34023  poimirlem18  34055  poimirlem21  34058  mblfinlem2  34075  itgabsnc  34106  itggt0cn  34109  prdsbnd  34218  prdstotbnd  34219  prdsbnd2  34220  rrnequiv  34260  eqlkr3  35257  dih1dimatlem  37485  fnwe2lem1  38583  imo72b2  39435  rfcnnnub  40132  disjxp1  40173  fompt  40306  fvixp2  40315  dmrelrnrel  40344  suplesup  40467  infxr  40495  monoord2xrv  40623  climinf  40750  climsuse  40752  mullimc  40760  limccog  40764  mullimcf  40767  limcperiod  40772  limcleqr  40788  neglimc  40791  0ellimcdiv  40793  limclner  40795  limsuppnfdlem  40845  limsupubuzlem  40856  xlimmnfvlem2  40977  xlimpnfvlem2  40981  climxlim2lem  40989  dvdivbd  41070  ioodvbdlimc1lem1  41078  dvnprodlem2  41094  iblsplit  41113  stoweidlem5  41153  stoweidlem16  41164  stoweidlem21  41169  stoweidlem24  41172  stoweidlem25  41173  stoweidlem28  41176  stoweidlem31  41179  stoweidlem41  41189  stoweidlem42  41190  stoweidlem44  41192  stoweidlem45  41193  stoweidlem48  41196  stoweidlem51  41199  stoweidlem54  41202  stoweidlem57  41205  stoweidlem60  41208  stoweidlem62  41210  stirlinglem5  41226  dirkercncflem3  41253  fourierdlem11  41266  fourierdlem12  41267  fourierdlem14  41269  fourierdlem15  41270  fourierdlem31  41286  fourierdlem34  41289  fourierdlem41  41296  fourierdlem48  41302  fourierdlem49  41303  fourierdlem50  41304  fourierdlem54  41308  fourierdlem69  41323  fourierdlem73  41327  fourierdlem74  41328  fourierdlem75  41329  fourierdlem76  41330  fourierdlem79  41333  fourierdlem80  41334  fourierdlem81  41335  fourierdlem92  41346  fourierdlem93  41347  fourierdlem94  41348  fourierdlem97  41351  fourierdlem103  41357  fourierdlem104  41358  fourierdlem111  41365  fourierdlem113  41367  etransclem32  41414  subsaliuncllem  41503  sge0rpcpnf  41566  caragendifcl  41659  iinhoiicclem  41818  pimdecfgtioc  41856  issmfgtlem  41895