Theorem r19.21bi 3173

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀wral 3106

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 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111

This theorem is referenced by:  r19.21be  3174  rspec2  3175  rspec3  3176  ralxfr2d  5276  fvmptelrn  6854  f1oresrab  6866  isoselem  7073  mpoexw  7759  boxcutc  8488  xpf1o  8663  fineqvlem  8716  indexfi  8816  dffi3  8879  suppr  8919  supiso  8923  infpr  8951  ordtypelem9  8974  brwdom3  9030  xpwdomg  9033  ixpiunwdom  9038  infxpenc2lem1  9430  hsmexlem4  9840  gchina  10110  wunom  10131  prcdnq  10404  prnmax  10406  dedekind  10792  dedekindle  10793  monoord2  13397  limsupgre  14830  limsupbnd1  14831  limsupbnd2  14832  climmpt2  14922  rlimcld2  14927  climsup  15018  sumpr  15095  sumtp  15096  fsum2dlem  15117  fsumiun  15168  fprod2dlem  15326  iserodd  16162  vdwlem1  16307  vdwlem6  16312  vdwnnlem3  16323  imasvscafn  16802  fuciso  17237  evlfcl  17464  yonedainv  17523  acsmapd  17780  prdsmndd  17936  psgnunilem5  18614  gsummpt1n0  19078  dprdspan  19142  ablfaclem2  19201  srgi  19254  srgrz  19269  srglz  19270  issrngd  19625  frgpcyg  20265  psrbaglesupp  20606  psrbagcon  20609  evlslem2  20751  mpfind  20779  gsumsmonply1  20932  gsummoncoe1  20933  evl1gsummon  20989  cpmatmcllem  21323  neiptoptop  21736  neiptopnei  21737  ordtrest2lem  21808  cncmp  21997  1stckgenlem  22158  ptcld  22218  dfac14  22223  ptcnplem  22226  pthaus  22243  xkococnlem  22264  xkococn  22265  cnmpt2k  22293  xpstopnlem1  22414  cnpflfi  22604  ptcmplem2  22658  cnextcn  22672  cnextfres1  22673  cnmpt2plusg  22693  cnmpt2vsca  22800  ustfilxp  22818  utoptop  22840  restutop  22843  restutopopn  22844  ucncn  22891  cfilufg  22899  trcfilu  22900  psmet0  22915  psmettri2  22916  prdsxmetlem  22975  prdsbl  23098  prdsxmslem2  23136  psmetutop  23174  cnmpt2ds  23448  bndth  23563  cnmpt2ip  23852  iscmet3lem2  23896  cmetcusp1  23957  rrxcph  23996  ovoliunlem1  24106  ovoliunlem3  24108  ovoliun  24109  ovoliun2  24110  ovolscalem1  24117  volfiniun  24151  uniioombllem4  24190  mbfeqalem1  24245  mbfres2  24249  ismbf3d  24258  mbfsup  24268  mbfinf  24269  mbflim  24272  itg1ge0  24290  itg1mulc  24308  itg1climres  24318  mbfi1fseqlem4  24322  itg2lea  24348  itg2splitlem  24352  itg2split  24353  itg2monolem1  24354  itg2mono  24357  itg2i1fseqle  24358  itg2i1fseq  24359  itg2addlem  24362  itg2cnlem1  24365  itgeqa  24417  itgfsum  24430  itgabs  24438  itggt0  24447  dvlipcn  24597  dvfsumabs  24626  dvfsumlem2  24630  itgsubstlem  24651  coeeulem  24821  dgrlem  24826  dgrlb  24833  coeaddlem  24846  coecj  24875  ulmss  24992  leibpi  25528  xrlimcnp  25554  o1cxp  25560  jensen  25574  lgambdd  25622  wilthlem2  25654  sqff1o  25767  fsumdvdscom  25770  fsumdvdsmul  25780  dchrmulcl  25833  dchrmulid2  25836  dchrinv  25845  dchrvmasumlem2  26082  ostth1  26217  ercgrg  26311  f1otrg  26665  f1otrge  26666  ubthlem2  28654  fmptcof2  30420  disjdsct  30462  fprodex01  30567  ccatf1  30651  ressprs  30668  oduprs  30669  gsumpart  30740  archiabl  30877  lmodslmd  30882  rhmimaidl  31017  fedgmullem2  31114  fedgmul  31115  txomap  31187  qtophaus  31189  locfinreflem  31193  ordtrest2NEWlem  31275  lmdvg  31306  prodindf  31392  esumcl  31399  esumeq2d  31406  esumnul  31417  hasheuni  31454  esumcvg  31455  esumcvgre  31460  insiga  31506  ldsysgenld  31529  ldgenpisyslem1  31532  measvunilem  31581  measvunilem0  31582  measdivcstALTV  31594  cntmeas  31595  voliune  31598  volfiniune  31599  1stmbfm  31628  2ndmbfm  31629  omssubadd  31668  difelcarsg  31678  inelcarsg  31679  eulerpartlems  31728  eulerpartlemsv3  31729  eulerpartlemgvv  31744  dstrvprob  31839  hashreprin  32001  reprgt  32002  breprexplemc  32013  circlemeth  32021  hgt750lema  32038  tgoldbachgtd  32043  bnj93  32245  bnj518  32268  bnj1489  32438  fnrelpredd  32472  subfacp1lem3  32542  subfacp1lem5  32544  erdszelem8  32558  ptpconn  32593  resconn  32606  cvmliftmolem2  32642  cvmlift2lem11  32673  cvmliftphtlem  32677  mclsax  32929  conway  33377  slerec  33390  fin2so  35044  poimirlem18  35075  poimirlem21  35078  mblfinlem2  35095  itgabsnc  35126  itggt0cn  35127  prdsbnd  35231  prdstotbnd  35232  prdsbnd2  35233  rrnequiv  35273  eqlkr3  36397  dih1dimatlem  38625  3factsumint  39313  fnwe2lem1  39994  imo72b2  40878  rfcnnnub  41665  disjxp1  41703  fompt  41819  disjinfi  41820  fvixp2  41827  dmrelrnrel  41856  suplesup  41971  infxr  41999  monoord2xrv  42123  climinf  42248  climsuse  42250  mullimc  42258  limccog  42262  mullimcf  42265  limcperiod  42270  limcleqr  42286  neglimc  42289  0ellimcdiv  42291  limclner  42293  limsuppnfdlem  42343  limsupubuzlem  42354  xlimmnfvlem2  42475  xlimpnfvlem2  42479  climxlim2lem  42487  dvdivbd  42565  ioodvbdlimc1lem1  42573  dvnprodlem2  42589  iblsplit  42608  stoweidlem5  42647  stoweidlem16  42658  stoweidlem21  42663  stoweidlem24  42666  stoweidlem25  42667  stoweidlem28  42670  stoweidlem31  42673  stoweidlem41  42683  stoweidlem42  42684  stoweidlem44  42686  stoweidlem45  42687  stoweidlem48  42690  stoweidlem51  42693  stoweidlem54  42696  stoweidlem57  42699  stoweidlem60  42702  stoweidlem62  42704  stirlinglem5  42720  dirkercncflem3  42747  fourierdlem11  42760  fourierdlem12  42761  fourierdlem14  42763  fourierdlem15  42764  fourierdlem31  42780  fourierdlem34  42783  fourierdlem41  42790  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem54  42802  fourierdlem69  42817  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem79  42827  fourierdlem80  42828  fourierdlem81  42829  fourierdlem92  42840  fourierdlem93  42841  fourierdlem94  42842  fourierdlem97  42845  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fourierdlem113  42861  etransclem32  42908  subsaliuncllem  42997  sge0rpcpnf  43060  caragendifcl  43153  iinhoiicclem  43312  pimdecfgtioc  43350  issmfgtlem  43389