Theorem r19.21bi 3251

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062

This theorem is referenced by:  r19.21be  3252  rspec2  3279  rspec3  3280  ralxfr2d  5410  fvmptelcdm  7133  fompt  7138  f1oresrab  7147  isoselem  7361  mpoexw  8103  naddsuc2  8739  boxcutc  8981  xpf1o  9179  fineqvlem  9298  indexfi  9400  dffi3  9471  suppr  9511  supiso  9515  infpr  9543  ordtypelem9  9566  brwdom3  9622  xpwdomg  9625  ixpiunwdom  9630  infxpenc2lem1  10059  hsmexlem4  10469  gchina  10739  wunom  10760  prcdnq  11033  prnmax  11035  dedekind  11424  dedekindle  11425  monoord2  14074  limsupgre  15517  limsupbnd1  15518  limsupbnd2  15519  climmpt2  15609  rlimcld2  15614  climsup  15706  sumpr  15784  sumtp  15785  fsum2dlem  15806  fsumiun  15857  fprod2dlem  16016  iserodd  16873  vdwlem1  17019  vdwlem6  17024  vdwnnlem3  17035  imasvscafn  17582  fuciso  18023  evlfcl  18267  yonedainv  18326  oduprs  18346  acsmapd  18599  prdsmndd  18783  psgnunilem5  19512  gsummpt1n0  19983  dprdspan  20047  ablfaclem2  20106  srgdilem  20189  srgrz  20204  srglz  20205  issrngd  20856  frgpcyg  21592  psrbaglesupp  21942  psrbagcon  21945  psrbagleadd1  21948  evlslem2  22103  mpfind  22131  psdmul  22170  ply1chr  22310  gsumsmonply1  22311  gsummoncoe1  22312  evl1gsummon  22369  cpmatmcllem  22724  neiptoptop  23139  neiptopnei  23140  ordtrest2lem  23211  cncmp  23400  1stckgenlem  23561  ptcld  23621  dfac14  23626  ptcnplem  23629  pthaus  23646  xkococnlem  23667  xkococn  23668  cnmpt2k  23696  xpstopnlem1  23817  cnpflfi  24007  ptcmplem2  24061  cnextcn  24075  cnextfres1  24076  cnmpt2plusg  24096  cnmpt2vsca  24203  ustfilxp  24221  utoptop  24243  restutop  24246  restutopopn  24247  ucncn  24294  cfilufg  24302  trcfilu  24303  psmet0  24318  psmettri2  24319  prdsxmetlem  24378  prdsbl  24504  prdsxmslem2  24542  psmetutop  24580  cnmpt2ds  24865  bndth  24990  cnmpt2ip  25282  iscmet3lem2  25326  cmetcusp1  25387  rrxcph  25426  ovoliunlem1  25537  ovoliunlem3  25539  ovoliun  25540  ovoliun2  25541  ovolscalem1  25548  volfiniun  25582  uniioombllem4  25621  mbfeqalem1  25676  mbfres2  25680  ismbf3d  25689  mbfsup  25699  mbfinf  25700  mbflim  25703  itg1ge0  25721  itg1mulc  25739  itg1climres  25749  mbfi1fseqlem4  25753  itg2lea  25779  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itg2mono  25788  itg2i1fseqle  25789  itg2i1fseq  25790  itg2addlem  25793  itg2cnlem1  25796  itgeqa  25849  itgfsum  25862  itgabs  25870  itggt0  25879  dvlipcn  26033  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  itgsubstlem  26089  coeeulem  26263  dgrlem  26268  dgrlb  26275  coeaddlem  26288  coecj  26318  coecjOLD  26320  ulmss  26440  leibpi  26985  xrlimcnp  27011  o1cxp  27018  jensen  27032  lgambdd  27080  wilthlem2  27112  sqff1o  27225  fsumdvdscom  27228  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  dchrmulcl  27293  dchrmullid  27296  dchrinv  27305  dchrvmasumlem2  27542  ostth1  27677  conway  27844  slerec  27864  ercgrg  28525  f1otrg  28879  f1otrge  28880  ubthlem2  30890  fmptcof2  32667  disjdsct  32712  fprodex01  32827  prodindf  32848  ccatf1  32933  ressprs  32954  mgcf1o  32993  chnccats1  33005  gsumpart  33060  archiabl  33205  lmodslmd  33210  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnsubrunlem2  33252  rhmimaidl  33460  gsummoncoe1fzo  33618  ply1gsumz  33619  fedgmullem2  33681  fedgmul  33682  txomap  33833  qtophaus  33835  locfinreflem  33839  ordtrest2NEWlem  33921  lmdvg  33952  zrhcntr  33980  esumcl  34031  esumeq2d  34038  esumnul  34049  hasheuni  34086  esumcvg  34087  esumcvgre  34092  insiga  34138  ldsysgenld  34161  ldgenpisyslem1  34164  measvunilem  34213  measvunilem0  34214  measdivcstALTV  34226  cntmeas  34227  voliune  34230  volfiniune  34231  1stmbfm  34262  2ndmbfm  34263  omssubadd  34302  difelcarsg  34312  inelcarsg  34313  eulerpartlems  34362  eulerpartlemsv3  34363  eulerpartlemgvv  34378  dstrvprob  34474  hashreprin  34635  reprgt  34636  breprexplemc  34647  circlemeth  34655  hgt750lema  34672  tgoldbachgtd  34677  bnj93  34877  bnj518  34900  bnj1489  35070  fnrelpredd  35103  subfacp1lem3  35187  subfacp1lem5  35189  erdszelem8  35203  ptpconn  35238  resconn  35251  cvmliftmolem2  35287  cvmlift2lem11  35318  cvmliftphtlem  35322  mclsax  35574  weiunfr  36468  fin2so  37614  poimirlem18  37645  poimirlem21  37648  mblfinlem2  37665  itgabsnc  37696  itggt0cn  37697  prdsbnd  37800  prdstotbnd  37801  prdsbnd2  37802  rrnequiv  37842  eqlkr3  39102  dih1dimatlem  41331  3factsumint  42026  aks6d1c5lem2  42139  fnwe2lem1  43062  cantnf2  43338  nadd1suc  43405  imo72b2  44185  rfcnnnub  45041  disjxp1  45074  disjinfi  45197  fvixp2  45204  dmrelrnrel  45231  fvmptelcdmf  45277  suplesup  45350  infxr  45378  monoord2xrv  45494  climinf  45621  climsuse  45623  mullimc  45631  limccog  45635  mullimcf  45638  limcperiod  45643  limcleqr  45659  neglimc  45662  0ellimcdiv  45664  limclner  45666  limsuppnfdlem  45716  limsupubuzlem  45727  xlimmnfvlem2  45848  xlimpnfvlem2  45852  climxlim2lem  45860  dvdivbd  45938  ioodvbdlimc1lem1  45946  dvnprodlem2  45962  iblsplit  45981  stoweidlem5  46020  stoweidlem16  46031  stoweidlem21  46036  stoweidlem24  46039  stoweidlem25  46040  stoweidlem28  46043  stoweidlem31  46046  stoweidlem41  46056  stoweidlem42  46057  stoweidlem44  46059  stoweidlem45  46060  stoweidlem48  46063  stoweidlem51  46066  stoweidlem54  46069  stoweidlem57  46072  stoweidlem60  46075  stoweidlem62  46077  stirlinglem5  46093  dirkercncflem3  46120  fourierdlem11  46133  fourierdlem12  46134  fourierdlem14  46136  fourierdlem15  46137  fourierdlem31  46153  fourierdlem34  46156  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem54  46175  fourierdlem69  46190  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem79  46200  fourierdlem80  46201  fourierdlem81  46202  fourierdlem92  46213  fourierdlem93  46214  fourierdlem94  46215  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem113  46234  etransclem32  46281  subsaliuncllem  46372  sge0rpcpnf  46436  caragendifcl  46529  iinhoiicclem  46688  pimdecfgtioc  46730  issmfgtlem  46770  ormklocald  46889  ormkglobd  46890  thincciso2  49104