Theorem r19.21bi 3249

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063

This theorem is referenced by:  r19.21be  3250  rspec2  3277  rspec3  3278  ralxfr2d  5407  fvmptelcdm  7108  f1oresrab  7120  isoselem  7333  mpoexw  8060  boxcutc  8931  xpf1o  9135  fineqvlem  9258  indexfi  9356  dffi3  9422  suppr  9462  supiso  9466  infpr  9494  ordtypelem9  9517  brwdom3  9573  xpwdomg  9576  ixpiunwdom  9581  infxpenc2lem1  10010  hsmexlem4  10420  gchina  10690  wunom  10711  prcdnq  10984  prnmax  10986  dedekind  11373  dedekindle  11374  monoord2  13995  limsupgre  15421  limsupbnd1  15422  limsupbnd2  15423  climmpt2  15513  rlimcld2  15518  climsup  15612  sumpr  15690  sumtp  15691  fsum2dlem  15712  fsumiun  15763  fprod2dlem  15920  iserodd  16764  vdwlem1  16910  vdwlem6  16915  vdwnnlem3  16926  imasvscafn  17479  fuciso  17924  evlfcl  18171  yonedainv  18230  acsmapd  18503  prdsmndd  18654  psgnunilem5  19355  gsummpt1n0  19825  dprdspan  19889  ablfaclem2  19948  srgdilem  20006  srgrz  20021  srglz  20022  issrngd  20457  frgpcyg  21113  psrbaglesupp  21459  psrbaglesuppOLD  21460  psrbagcon  21465  psrbagconOLD  21466  evlslem2  21624  mpfind  21652  gsumsmonply1  21809  gsummoncoe1  21810  evl1gsummon  21866  cpmatmcllem  22202  neiptoptop  22617  neiptopnei  22618  ordtrest2lem  22689  cncmp  22878  1stckgenlem  23039  ptcld  23099  dfac14  23104  ptcnplem  23107  pthaus  23124  xkococnlem  23145  xkococn  23146  cnmpt2k  23174  xpstopnlem1  23295  cnpflfi  23485  ptcmplem2  23539  cnextcn  23553  cnextfres1  23554  cnmpt2plusg  23574  cnmpt2vsca  23681  ustfilxp  23699  utoptop  23721  restutop  23724  restutopopn  23725  ucncn  23772  cfilufg  23780  trcfilu  23781  psmet0  23796  psmettri2  23797  prdsxmetlem  23856  prdsbl  23982  prdsxmslem2  24020  psmetutop  24058  cnmpt2ds  24341  bndth  24456  cnmpt2ip  24747  iscmet3lem2  24791  cmetcusp1  24852  rrxcph  24891  ovoliunlem1  25001  ovoliunlem3  25003  ovoliun  25004  ovoliun2  25005  ovolscalem1  25012  volfiniun  25046  uniioombllem4  25085  mbfeqalem1  25140  mbfres2  25144  ismbf3d  25153  mbfsup  25163  mbfinf  25164  mbflim  25167  itg1ge0  25185  itg1mulc  25204  itg1climres  25214  mbfi1fseqlem4  25218  itg2lea  25244  itg2splitlem  25248  itg2split  25249  itg2monolem1  25250  itg2mono  25253  itg2i1fseqle  25254  itg2i1fseq  25255  itg2addlem  25258  itg2cnlem1  25261  itgeqa  25313  itgfsum  25326  itgabs  25334  itggt0  25343  dvlipcn  25493  dvfsumabs  25522  dvfsumlem2  25526  itgsubstlem  25547  coeeulem  25720  dgrlem  25725  dgrlb  25732  coeaddlem  25745  coecj  25774  ulmss  25891  leibpi  26427  xrlimcnp  26453  o1cxp  26459  jensen  26473  lgambdd  26521  wilthlem2  26553  sqff1o  26666  fsumdvdscom  26669  fsumdvdsmul  26679  dchrmulcl  26732  dchrmullid  26735  dchrinv  26744  dchrvmasumlem2  26981  ostth1  27116  conway  27280  slerec  27300  ercgrg  27748  f1otrg  28102  f1otrge  28103  ubthlem2  30102  fmptcof2  31860  disjdsct  31902  fprodex01  32009  ccatf1  32093  ressprs  32111  oduprs  32112  mgcf1o  32151  gsumpart  32185  archiabl  32322  lmodslmd  32327  rhmimaidl  32508  ply1chr  32608  gsummoncoe1fzo  32615  ply1gsumz  32616  fedgmullem2  32660  fedgmul  32661  txomap  32752  qtophaus  32754  locfinreflem  32758  ordtrest2NEWlem  32840  lmdvg  32871  prodindf  32959  esumcl  32966  esumeq2d  32973  esumnul  32984  hasheuni  33021  esumcvg  33022  esumcvgre  33027  insiga  33073  ldsysgenld  33096  ldgenpisyslem1  33099  measvunilem  33148  measvunilem0  33149  measdivcstALTV  33161  cntmeas  33162  voliune  33165  volfiniune  33166  1stmbfm  33197  2ndmbfm  33198  omssubadd  33237  difelcarsg  33247  inelcarsg  33248  eulerpartlems  33297  eulerpartlemsv3  33298  eulerpartlemgvv  33313  dstrvprob  33408  hashreprin  33570  reprgt  33571  breprexplemc  33582  circlemeth  33590  hgt750lema  33607  tgoldbachgtd  33612  bnj93  33812  bnj518  33835  bnj1489  34005  fnrelpredd  34030  subfacp1lem3  34111  subfacp1lem5  34113  erdszelem8  34127  ptpconn  34162  resconn  34175  cvmliftmolem2  34211  cvmlift2lem11  34242  cvmliftphtlem  34246  mclsax  34498  gg-dvfsumlem2  35121  fin2so  36413  poimirlem18  36444  poimirlem21  36447  mblfinlem2  36464  itgabsnc  36495  itggt0cn  36496  prdsbnd  36599  prdstotbnd  36600  prdsbnd2  36601  rrnequiv  36641  eqlkr3  37909  dih1dimatlem  40138  3factsumint  40828  fnwe2lem1  41725  cantnf2  42008  nadd1suc  42075  naddsuc2  42076  imo72b2  42857  rfcnnnub  43653  disjxp1  43689  fompt  43823  disjinfi  43824  fvixp2  43831  dmrelrnrel  43858  fvmptelcdmf  43910  suplesup  43984  infxr  44012  monoord2xrv  44129  climinf  44257  climsuse  44259  mullimc  44267  limccog  44271  mullimcf  44274  limcperiod  44279  limcleqr  44295  neglimc  44298  0ellimcdiv  44300  limclner  44302  limsuppnfdlem  44352  limsupubuzlem  44363  xlimmnfvlem2  44484  xlimpnfvlem2  44488  climxlim2lem  44496  dvdivbd  44574  ioodvbdlimc1lem1  44582  dvnprodlem2  44598  iblsplit  44617  stoweidlem5  44656  stoweidlem16  44667  stoweidlem21  44672  stoweidlem24  44675  stoweidlem25  44676  stoweidlem28  44679  stoweidlem31  44682  stoweidlem41  44692  stoweidlem42  44693  stoweidlem44  44695  stoweidlem45  44696  stoweidlem48  44699  stoweidlem51  44702  stoweidlem54  44705  stoweidlem57  44708  stoweidlem60  44711  stoweidlem62  44713  stirlinglem5  44729  dirkercncflem3  44756  fourierdlem11  44769  fourierdlem12  44770  fourierdlem14  44772  fourierdlem15  44773  fourierdlem31  44789  fourierdlem34  44792  fourierdlem41  44799  fourierdlem48  44805  fourierdlem49  44806  fourierdlem50  44807  fourierdlem54  44811  fourierdlem69  44826  fourierdlem73  44830  fourierdlem74  44831  fourierdlem75  44832  fourierdlem76  44833  fourierdlem79  44836  fourierdlem80  44837  fourierdlem81  44838  fourierdlem92  44849  fourierdlem93  44850  fourierdlem94  44851  fourierdlem97  44854  fourierdlem103  44860  fourierdlem104  44861  fourierdlem111  44868  fourierdlem113  44870  etransclem32  44917  subsaliuncllem  45008  sge0rpcpnf  45072  caragendifcl  45165  iinhoiicclem  45324  pimdecfgtioc  45366  issmfgtlem  45406