Theorem ralrimiva 2623

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)

Hypothesis

Ref	Expression
ralrimiva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Assertion

Ref	Expression
ralrimiva	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimiva

Step	Hyp	Ref	Expression
1		ralrimiva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)
2	1	ex 115	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralrimiv 2622	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralrimivvva  2633  rgen2  2636  rgen3  2637  nrexdv  2643  r19.29vva  2696  rabbidva  2809  ssrabdv  3327  ss2rabdv  3329  iuneq2dv  4033  iunssd  4058  disjeq2dv  4111  mpteq12dva  4212  triun  4242  issod  4464  frirrg  4495  frind  4497  peano2  4742  dmmptd  5514  fun11iun  5660  fniinfv  5761  eqfnfv  5806  eqfnfvd  5809  fnmptfvd  5813  dff3im  5853  dffo4  5856  fmptd  5862  ffnfv  5866  fmpt2d  5870  ffvresb  5871  funiun  5890  fconst2g  5930  fconstfvm  5933  resfunexg  5936  eufnfv  5949  foco2  5959  fniunfv  5968  fcofo  5990  fliftel  5999  fliftfun  6002  fliftfuns  6004  riota5f  6065  f1ocnvd  6292  f1o3d  6298  suppssov1  6299  offval2  6318  ofrfval2  6319  offveqb  6322  offveq  6323  caofref  6327  caofinvl  6328  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  opabex3d  6350  uchoice  6371  oprssdmm  6405  f1od2  6471  disjxp1  6472  funsssuppss  6498  suppofss1dcl  6504  suppofss2dcl  6505  tfrlem1  6579  tfrlemisucaccv  6596  tfrlemiubacc  6601  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemubacc  6617  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemubacc  6630  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  rdgon  6657  freccllem  6673  frecfcllem  6675  omcl  6734  oeicl  6735  qliftfuns  6893  ixpeq2dva  6995  xpf1o  7144  mapxpen  7148  isinfinf  7201  fimax2gtrilemstep  7205  undifdcss  7230  opabfi  7247  fissfi  7263  fdcf1  7316  f1setfi  7317  2omap  7319  eqsuptid  7338  eqinftid  7362  difinfsnlem  7440  difinfsn  7441  ctmlemr  7449  ctm  7450  ctssdclemn0  7451  ctssdccl  7452  enumctlemm  7455  nninfninc  7464  nnnninf  7467  nnnninfeq  7469  enomnilem  7479  ismkvnex  7496  enmkvlem  7502  enwomnilem  7510  nninfwlporlemd  7513  nninfwlpoimlemg  7516  nninfwlpoimlemginf  7517  nninfwlpoim  7520  nninfinfwlpo  7521  finacn  7561  acfun  7564  exmidaclem  7565  exmidontriimlem4  7581  exmidontriim  7582  pw1on  7586  ccfunen  7631  cc2lem  7633  cc3  7635  acnccim  7639  genprndl  7889  genprndu  7890  nqprloc  7913  ltexprlemrnd  7973  ltexprlemdisj  7974  lteupri  7985  recexprlemrnd  7997  recexprlemdisj  7998  caucvgprlemlim  8049  caucvgprprlemlim  8079  suplocexprlemml  8084  suplocexprlemrl  8085  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  caucvgsrlembound  8162  caucvgsrlemgt1  8163  caucvgsrlemoffgt1  8167  caucvgsr  8170  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  elrealeu  8197  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  negeu  8519  eqord1  8813  eqord2  8814  creur  9292  creui  9293  suprzclex  9749  supinfneg  10005  infsupneg  10006  infregelbex  10008  indstr2  10019  irraddap  10057  iooidg  10322  iccsupr  10379  icoshftf1o  10404  fznlem  10456  exfzdc  10670  zsupcllemstep  10673  infssuzex  10677  suprzubdc  10682  zsupssdc  10684  exbtwnzlemstep  10693  exbtwnzlemex  10695  frec2uzrdg  10861  frecuzrdgrcl  10862  frecuzrdgtcl  10864  frecuzrdgsuc  10866  frecuzrdgrclt  10867  frecuzrdgg  10868  frecuzrdgfunlem  10871  frecuzrdgsuctlem  10875  nninfinf  10895  iseqovex  10910  seq3val  10912  seqvalcd  10913  seq3-1  10914  seqf  10916  seq3p1  10917  seqovcd  10919  seqp1cd  10922  seq3clss  10923  seq3fveq2  10927  seqfveq2g  10929  seqfveqg  10930  seq3fveq  10931  seq3feq  10932  seq3shft2  10933  seqshft2g  10934  monoord  10937  monoord2  10938  ser3mono  10939  seq3split  10940  seqsplitg  10941  seq3caopr3  10943  seqcaopr3g  10944  seq3caopr2  10945  seqcaopr2g  10946  iseqf1olemqk  10959  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  iseqf1olemfvp  10962  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  seq3f1oleml  10968  seq3f1o  10969  seqf1og  10973  seq3id3  10976  seq3id  10977  seq3id2  10978  seq3homo  10979  seq3z  10980  seqhomog  10982  seqfeq4g  10983  ser3ge0  10988  nn0ltexp2  11163  bccl  11221  hashinfuni  11232  hashennnuni  11234  sshashneg  11297  hashfibclem  11298  hashf1lem1  11301  wrdexg  11331  ccatlen  11379  ccatvalfn  11385  ccatrn  11393  swrdlen  11440  swrdwrdsymbg  11452  swrdswrd  11493  wrdind  11510  reuccatpfxs1  11535  shftf  11611  seq3shft  11619  caucvgrelemcau  11762  cvg1nlemcau  11766  cvg1nlemres  11767  resqrexlemcvg  11801  resqrexlemglsq  11804  resqrexlemga  11805  maxabslemval  11991  negfi  12011  minmax  12014  xrmaxiflemval  12035  xrminmax  12050  climconst  12075  2clim  12086  climcn1  12093  climcn2  12094  reccn2ap  12098  cn1lem  12099  climsqz  12120  climsqz2  12121  climcau  12132  climrecvg1n  12133  serf0  12137  sumeq2dv  12153  sumrbdclem  12163  fsum3cvg  12164  summodclem3  12166  summodclem2a  12167  zsumdc  12170  isum  12171  fsumgcl  12172  fsum3  12173  fsumf1o  12176  isumss  12177  fisumss  12178  isumss2  12179  fsum3cvg2  12180  fsumsersdc  12181  fsum3ser  12183  fsumcl2lem  12184  fsumadd  12192  fsumsplit  12193  fsumm1  12202  fsum1p  12204  isumclim3  12209  isummulc2  12212  sumsplitdc  12218  fsum2dlemstep  12220  fisumcom2  12224  fsumshftm  12231  fsummulc2  12234  fsumge1  12247  fsum00  12248  fsumabs  12251  telfsumo  12252  telfsumo2  12253  fsumparts  12256  fsumrelem  12257  fsumiun  12263  hashiun  12264  hash2iun  12265  binomlem  12269  isumshft  12276  isum1p  12278  isumnn0nn  12279  isumrpcl  12280  isumlessdc  12282  divcnv  12283  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemseq  12312  cvgratnnlemabsle  12313  cvgratnnlemfm  12315  cvgratnnlemrate  12316  cvgratnn  12317  cvgratz  12318  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  clim2prod  12325  prodeq2dv  12352  prodrbdclem  12357  fproddccvg  12358  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  iprodap  12366  fprodseq  12369  fprodf1o  12374  prodssdc  12375  fprodssdc  12376  fprodmul  12377  fprodsplit  12383  fprodm1  12384  fprod1p  12385  fprodm1s  12387  fprodp1s  12388  fprodunsn  12390  fprodcl2lem  12391  fprodabs  12402  fprodeq0  12403  fprodap0  12407  fprod2dlemstep  12408  fprodcom2fi  12412  fprodrec  12415  fprodmodd  12427  efcvgfsum  12453  dvdsssfz1  12638  bitsfi  12743  bitsinv1  12748  dvdsbnd  12752  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlemle  12804  bezoutlemsup  12805  dfgcd3  12806  dfgcd2  12810  nnwodc  12832  uzwodc  12833  nnwosdc  12835  nninfctlemfo  12836  coprmgcdb  12885  prmdc  12927  isprm5  12940  isprm6  12945  phivalfi  13013  phibndlem  13017  dfphi2  13021  hashdvds  13022  phiprmpw  13023  phimullem  13026  eulerthlemfi  13029  dvdsfi  13040  hashgcdeq  13041  phisum  13042  reumodprminv  13055  pclemdc  13090  pc2dvds  13132  pcz  13134  pcprmpw2  13135  pcmptdvds  13147  pcprod  13148  pcfac  13152  qexpz  13154  prmpwdvds  13157  pockthg  13159  infpnlem2  13162  1arithlem4  13168  1arith  13169  4sqlemafi  13197  4sqlemffi  13198  4sqleminfi  13199  ballotfilemcinfi  13276  ballotfilemdifcfi  13277  ballotfilemcinfz  13278  ballotfilemdifcfz  13279  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemefi  13289  ballotfilemodife  13292  ballotfilemiex  13296  ennnfonelemex  13357  ennnfonelemfun  13360  ennnfonelemf1  13361  ennnfonelemnn0  13365  ennnfonelemim  13367  exmidunben  13369  ctinfomlemom  13370  ctinfom  13371  ctinf  13373  ctiunctlemudc  13380  ctiunctlemf  13381  ctiunctlemfo  13382  omctfn  13386  ssnnctlemct  13389  nninfdclemcl  13391  nninfdclemp1  13393  imasival  13680  ismgmid2  13753  mgmidsssn0  13757  grpinvalem  13758  grpinva  13759  gzsumress  13765  issgrpd  13780  sgrpidmndm  13786  ismndd  13803  mndpfo  13804  mhmima  13851  mhmeql  13852  gsumvallem2  13853  isgrpd2e  13878  dfgrp2  13885  grpidd2  13899  isgrpinv  13912  grplrinv  13915  grpidinv  13917  dfgrp3me  13958  mhmmnd  13972  ghmgrp  13974  mulgsubcl  13992  issubg2m  14045  issubgrpd2  14046  grpissubg  14050  subgintm  14054  nmzsubg  14066  ssnmz  14067  ghmrn  14113  ghmeql  14123  ghmf1  14129  conjnmz  14135  conjnmzb  14136  cntzsgrpcl  14161  cntz2ss  14162  cntzsubm  14164  cntzsubg  14165  cntzmhm  14167  cntzmhm2  14168  rinvmod  14197  gsummptfidmadd  14245  prdsplusgsgrpcl  14274  prdsplusgcl  14276  prdsidlem  14277  prdsinvlem  14280  pwsbas  14289  srgrz  14372  srglz  14373  srgisid  14374  ringsrg  14436  rhmdvdsr  14566  rhmopp  14567  subrngintm  14604  subrg1  14623  subrgugrp  14632  subrgintm  14635  rrgsupp  14658  unitrrg  14660  aprap  14682  islmodd  14713  lssuni  14784  lsssubg  14798  lssintclm  14805  dflidl2rng  14902  lidlsubg  14907  cnsubglem  15000  gsumfsum  15007  znf1o  15070  znidomb  15077  asclfnd  15107  psrbagfi  15143  psrbaglecl  15144  psrbagcon  15146  psrbaglefifi  15147  psr1clfi  15170  mplsubgfilemm  15180  mplsubgfilemcl  15181  mplsubgfi  15183  fiinbas  15241  tgclb  15257  restbasg  15360  iscnp4  15410  cnco  15413  cnptopco  15414  cnss1  15418  cnss2  15419  cncnpi  15420  cncnp  15422  cnconst2  15425  cnrest  15427  cnptopresti  15430  cnpdis  15434  lmtopcnp  15442  txbasval  15459  tx1cn  15461  tx2cn  15462  txcnp  15463  upxp  15464  txdis1cn  15470  cnmpt11  15475  psmet0  15519  psmettri2  15520  psmetxrge0  15524  psmetres2  15525  ismeti  15538  xmetpsmet  15561  blsscls2  15685  comet  15691  xmettx  15702  tgioo  15746  tgqioo  15747  fsumcncntop  15759  elcncf1di  15771  cdivcncfap  15796  mulcncflem  15799  mulcncf  15800  cnopnap  15803  divcncfap  15806  dedekindeulemuub  15809  dedekindeulemlu  15813  suplociccreex  15816  suplociccex  15817  dedekindicclemuub  15818  dedekindicclemlu  15822  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemdisj  15832  ivthinclemloc  15833  ivthinc  15835  ivthdec  15836  dich0  15844  ivthdich  15845  cnplimclemr  15861  limccnp2cntop  15869  limccoap  15870  dvcn  15892  dvfre  15902  dvrecap  15905  dvmptclx  15910  dvmptaddx  15911  dvmptmulx  15912  dveflem  15918  dvef  15919  ply1termlem  15934  plyaddlem1  15939  plymullem1  15940  plycoeid3  15949  plycj  15953  plyreres  15956  dvply1  15957  sin0pilem1  15974  sin0pilem2  15975  zprmlogbaplem2  16177  ppiqfi  16203  prmdvdsfi  16204  ppiprm  16220  chtprm  16222  chtdif  16225  efchtqdvds  16226  ppidif  16230  prmorcht  16243  mpodvdsmulf1o  16245  ppiqub  16254  chtublem  16256  mersenne  16258  perfectlem2  16261  bposlem1  16272  bposlem3  16274  bposlem5  16276  bposlem6  16277  lgsval2lem  16295  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem1f1o  16345  gausslemma2dlem2  16347  gausslemma2dlem3  16348  lgsquadlemofi  16361  lgsquadlem1  16362  lgsquadlem2  16363  2lgslem1a1  16371  2sqlem6  16405  2sqlem8  16408  2sqlem10  16410  usgruspgrben  16593  uspgredg2v  16628  usgredg2v  16631  subuhgr  16679  subupgr  16680  subumgr  16681  subusgr  16682  vtxedgfi  16696  vtxlpfi  16697  wlk1walkdom  16766  wlkres  16786  eupth2lembfi  16884  depindlem1  16913  depindlem2  16914  depindlem3  16915  dichmul0or  16926  fnmptd  16998  bj-charfun  16999  bj-charfundc  17000  bj-charfunr  17002  pw1nct  17199  wexmiddiffi  17210  nnsf  17214  nninfalllem1  17217  nninfall  17218  nninfself  17222  nninfsellemeq  17223  nninfsellemeqinf  17225  nninfsel  17226  nnnninfex  17231  nninfnfiinf  17232  repiecef  17243  isomninnlem  17245  trilpolemeq1  17256  trilpo  17259  apdiff  17264  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269  redcwlpo  17272  redc0  17274  reap0  17275  dceqnconst  17277  dcapnconst  17278  nconstwlpolem  17282  nconstwlpo  17283  neapmkv  17285  ltlenmkv  17287