Theorem r19.21bi 3248

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3062

This theorem is referenced by:  r19.21be  3249  rspec2  3276  rspec3  3277  ralxfr2d  5408  fvmptelcdm  7114  fompt  7119  f1oresrab  7127  isoselem  7340  mpoexw  8067  boxcutc  8937  xpf1o  9141  fineqvlem  9264  indexfi  9362  dffi3  9428  suppr  9468  supiso  9472  infpr  9500  ordtypelem9  9523  brwdom3  9579  xpwdomg  9582  ixpiunwdom  9587  infxpenc2lem1  10016  hsmexlem4  10426  gchina  10696  wunom  10717  prcdnq  10990  prnmax  10992  dedekind  11379  dedekindle  11380  monoord2  14001  limsupgre  15427  limsupbnd1  15428  limsupbnd2  15429  climmpt2  15519  rlimcld2  15524  climsup  15618  sumpr  15696  sumtp  15697  fsum2dlem  15718  fsumiun  15769  fprod2dlem  15926  iserodd  16770  vdwlem1  16916  vdwlem6  16921  vdwnnlem3  16932  imasvscafn  17485  fuciso  17930  evlfcl  18177  yonedainv  18236  acsmapd  18509  prdsmndd  18660  psgnunilem5  19364  gsummpt1n0  19835  dprdspan  19899  ablfaclem2  19958  srgdilem  20017  srgrz  20032  srglz  20033  issrngd  20473  frgpcyg  21135  psrbaglesupp  21483  psrbaglesuppOLD  21484  psrbagcon  21489  psrbagconOLD  21490  evlslem2  21648  mpfind  21676  gsumsmonply1  21834  gsummoncoe1  21835  evl1gsummon  21891  cpmatmcllem  22227  neiptoptop  22642  neiptopnei  22643  ordtrest2lem  22714  cncmp  22903  1stckgenlem  23064  ptcld  23124  dfac14  23129  ptcnplem  23132  pthaus  23149  xkococnlem  23170  xkococn  23171  cnmpt2k  23199  xpstopnlem1  23320  cnpflfi  23510  ptcmplem2  23564  cnextcn  23578  cnextfres1  23579  cnmpt2plusg  23599  cnmpt2vsca  23706  ustfilxp  23724  utoptop  23746  restutop  23749  restutopopn  23750  ucncn  23797  cfilufg  23805  trcfilu  23806  psmet0  23821  psmettri2  23822  prdsxmetlem  23881  prdsbl  24007  prdsxmslem2  24045  psmetutop  24083  cnmpt2ds  24366  bndth  24481  cnmpt2ip  24772  iscmet3lem2  24816  cmetcusp1  24877  rrxcph  24916  ovoliunlem1  25026  ovoliunlem3  25028  ovoliun  25029  ovoliun2  25030  ovolscalem1  25037  volfiniun  25071  uniioombllem4  25110  mbfeqalem1  25165  mbfres2  25169  ismbf3d  25178  mbfsup  25188  mbfinf  25189  mbflim  25192  itg1ge0  25210  itg1mulc  25229  itg1climres  25239  mbfi1fseqlem4  25243  itg2lea  25269  itg2splitlem  25273  itg2split  25274  itg2monolem1  25275  itg2mono  25278  itg2i1fseqle  25279  itg2i1fseq  25280  itg2addlem  25283  itg2cnlem1  25286  itgeqa  25338  itgfsum  25351  itgabs  25359  itggt0  25368  dvlipcn  25518  dvfsumabs  25547  dvfsumlem2  25551  itgsubstlem  25572  coeeulem  25745  dgrlem  25750  dgrlb  25757  coeaddlem  25770  coecj  25799  ulmss  25916  leibpi  26454  xrlimcnp  26480  o1cxp  26486  jensen  26500  lgambdd  26548  wilthlem2  26580  sqff1o  26693  fsumdvdscom  26696  fsumdvdsmul  26706  dchrmulcl  26759  dchrmullid  26762  dchrinv  26771  dchrvmasumlem2  27008  ostth1  27143  conway  27308  slerec  27328  ercgrg  27806  f1otrg  28160  f1otrge  28161  ubthlem2  30162  fmptcof2  31920  disjdsct  31962  fprodex01  32069  ccatf1  32153  ressprs  32171  oduprs  32172  mgcf1o  32211  gsumpart  32248  archiabl  32385  lmodslmd  32390  rhmimaidl  32595  ply1chr  32706  gsummoncoe1fzo  32714  ply1gsumz  32715  fedgmullem2  32774  fedgmul  32775  txomap  32883  qtophaus  32885  locfinreflem  32889  ordtrest2NEWlem  32971  lmdvg  33002  prodindf  33090  esumcl  33097  esumeq2d  33104  esumnul  33115  hasheuni  33152  esumcvg  33153  esumcvgre  33158  insiga  33204  ldsysgenld  33227  ldgenpisyslem1  33230  measvunilem  33279  measvunilem0  33280  measdivcstALTV  33292  cntmeas  33293  voliune  33296  volfiniune  33297  1stmbfm  33328  2ndmbfm  33329  omssubadd  33368  difelcarsg  33378  inelcarsg  33379  eulerpartlems  33428  eulerpartlemsv3  33429  eulerpartlemgvv  33444  dstrvprob  33539  hashreprin  33701  reprgt  33702  breprexplemc  33713  circlemeth  33721  hgt750lema  33738  tgoldbachgtd  33743  bnj93  33943  bnj518  33966  bnj1489  34136  fnrelpredd  34161  subfacp1lem3  34242  subfacp1lem5  34244  erdszelem8  34258  ptpconn  34293  resconn  34306  cvmliftmolem2  34342  cvmlift2lem11  34373  cvmliftphtlem  34377  mclsax  34629  gg-dvfsumlem2  35252  fin2so  36561  poimirlem18  36592  poimirlem21  36595  mblfinlem2  36612  itgabsnc  36643  itggt0cn  36644  prdsbnd  36747  prdstotbnd  36748  prdsbnd2  36749  rrnequiv  36789  eqlkr3  38057  dih1dimatlem  40286  3factsumint  40976  fnwe2lem1  41874  cantnf2  42157  nadd1suc  42224  naddsuc2  42225  imo72b2  43006  rfcnnnub  43802  disjxp1  43838  disjinfi  43970  fvixp2  43977  dmrelrnrel  44004  fvmptelcdmf  44054  suplesup  44128  infxr  44156  monoord2xrv  44273  climinf  44401  climsuse  44403  mullimc  44411  limccog  44415  mullimcf  44418  limcperiod  44423  limcleqr  44439  neglimc  44442  0ellimcdiv  44444  limclner  44446  limsuppnfdlem  44496  limsupubuzlem  44507  xlimmnfvlem2  44628  xlimpnfvlem2  44632  climxlim2lem  44640  dvdivbd  44718  ioodvbdlimc1lem1  44726  dvnprodlem2  44742  iblsplit  44761  stoweidlem5  44800  stoweidlem16  44811  stoweidlem21  44816  stoweidlem24  44819  stoweidlem25  44820  stoweidlem28  44823  stoweidlem31  44826  stoweidlem41  44836  stoweidlem42  44837  stoweidlem44  44839  stoweidlem45  44840  stoweidlem48  44843  stoweidlem51  44846  stoweidlem54  44849  stoweidlem57  44852  stoweidlem60  44855  stoweidlem62  44857  stirlinglem5  44873  dirkercncflem3  44900  fourierdlem11  44913  fourierdlem12  44914  fourierdlem14  44916  fourierdlem15  44917  fourierdlem31  44933  fourierdlem34  44936  fourierdlem41  44943  fourierdlem48  44949  fourierdlem49  44950  fourierdlem50  44951  fourierdlem54  44955  fourierdlem69  44970  fourierdlem73  44974  fourierdlem74  44975  fourierdlem75  44976  fourierdlem76  44977  fourierdlem79  44980  fourierdlem80  44981  fourierdlem81  44982  fourierdlem92  44993  fourierdlem93  44994  fourierdlem94  44995  fourierdlem97  44998  fourierdlem103  45004  fourierdlem104  45005  fourierdlem111  45012  fourierdlem113  45014  etransclem32  45061  subsaliuncllem  45152  sge0rpcpnf  45216  caragendifcl  45309  iinhoiicclem  45468  pimdecfgtioc  45510  issmfgtlem  45550