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  7318  eqsuptid  7337  eqinftid  7361  difinfsnlem  7439  difinfsn  7440  ctmlemr  7448  ctm  7449  ctssdclemn0  7450  ctssdccl  7451  enumctlemm  7454  nninfninc  7463  nnnninf  7466  nnnninfeq  7468  enomnilem  7478  ismkvnex  7495  enmkvlem  7501  enwomnilem  7509  nninfwlporlemd  7512  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  nninfwlpoim  7519  nninfinfwlpo  7520  finacn  7560  acfun  7563  exmidaclem  7564  exmidontriimlem4  7580  exmidontriim  7581  pw1on  7585  ccfunen  7630  cc2lem  7632  cc3  7634  acnccim  7638  genprndl  7888  genprndu  7889  nqprloc  7912  ltexprlemrnd  7972  ltexprlemdisj  7973  lteupri  7984  recexprlemrnd  7996  recexprlemdisj  7997  caucvgprlemlim  8048  caucvgprprlemlim  8078  suplocexprlemml  8083  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  caucvgsrlembound  8161  caucvgsrlemgt1  8162  caucvgsrlemoffgt1  8166  caucvgsr  8169  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  elrealeu  8196  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  negeu  8518  eqord1  8812  eqord2  8813  creur  9291  creui  9292  suprzclex  9748  supinfneg  10004  infsupneg  10005  infregelbex  10007  indstr2  10018  irraddap  10056  iooidg  10321  iccsupr  10378  icoshftf1o  10403  fznlem  10455  exfzdc  10669  zsupcllemstep  10672  infssuzex  10676  suprzubdc  10681  zsupssdc  10683  exbtwnzlemstep  10692  exbtwnzlemex  10694  frec2uzrdg  10859  frecuzrdgrcl  10860  frecuzrdgtcl  10862  frecuzrdgsuc  10864  frecuzrdgrclt  10865  frecuzrdgg  10866  frecuzrdgfunlem  10869  frecuzrdgsuctlem  10873  nninfinf  10893  iseqovex  10908  seq3val  10910  seqvalcd  10911  seq3-1  10912  seqf  10914  seq3p1  10915  seqovcd  10917  seqp1cd  10920  seq3clss  10921  seq3fveq2  10925  seqfveq2g  10927  seqfveqg  10928  seq3fveq  10929  seq3feq  10930  seq3shft2  10931  seqshft2g  10932  monoord  10935  monoord2  10936  ser3mono  10937  seq3split  10938  seqsplitg  10939  seq3caopr3  10941  seqcaopr3g  10942  seq3caopr2  10943  seqcaopr2g  10944  iseqf1olemqk  10957  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  iseqf1olemfvp  10960  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  seq3f1oleml  10966  seq3f1o  10967  seqf1og  10971  seq3id3  10974  seq3id  10975  seq3id2  10976  seq3homo  10977  seq3z  10978  seqhomog  10980  seqfeq4g  10981  ser3ge0  10986  nn0ltexp2  11161  bccl  11219  hashinfuni  11230  hashennnuni  11232  sshashneg  11295  hashfibclem  11296  hashf1lem1  11299  wrdexg  11329  ccatlen  11377  ccatvalfn  11383  ccatrn  11391  swrdlen  11438  swrdwrdsymbg  11450  swrdswrd  11491  wrdind  11508  reuccatpfxs1  11533  shftf  11609  seq3shft  11617  caucvgrelemcau  11760  cvg1nlemcau  11764  cvg1nlemres  11765  resqrexlemcvg  11799  resqrexlemglsq  11802  resqrexlemga  11803  maxabslemval  11989  negfi  12009  minmax  12011  xrmaxiflemval  12032  xrminmax  12047  climconst  12072  2clim  12083  climcn1  12090  climcn2  12091  reccn2ap  12095  cn1lem  12096  climsqz  12117  climsqz2  12118  climcau  12129  climrecvg1n  12130  serf0  12134  sumeq2dv  12150  sumrbdclem  12160  fsum3cvg  12161  summodclem3  12163  summodclem2a  12164  zsumdc  12167  isum  12168  fsumgcl  12169  fsum3  12170  fsumf1o  12173  isumss  12174  fisumss  12175  isumss2  12176  fsum3cvg2  12177  fsumsersdc  12178  fsum3ser  12180  fsumcl2lem  12181  fsumadd  12189  fsumsplit  12190  fsumm1  12199  fsum1p  12201  isumclim3  12206  isummulc2  12209  sumsplitdc  12215  fsum2dlemstep  12217  fisumcom2  12221  fsumshftm  12228  fsummulc2  12231  fsumge1  12244  fsum00  12245  fsumabs  12248  telfsumo  12249  telfsumo2  12250  fsumparts  12253  fsumrelem  12254  fsumiun  12260  hashiun  12261  hash2iun  12262  binomlem  12266  isumshft  12273  isum1p  12275  isumnn0nn  12276  isumrpcl  12277  isumlessdc  12279  divcnv  12280  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratnnlemseq  12309  cvgratnnlemabsle  12310  cvgratnnlemfm  12312  cvgratnnlemrate  12313  cvgratnn  12314  cvgratz  12315  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  clim2prod  12322  prodeq2dv  12349  prodrbdclem  12354  fproddccvg  12355  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  iprodap  12363  fprodseq  12366  fprodf1o  12371  prodssdc  12372  fprodssdc  12373  fprodmul  12374  fprodsplit  12380  fprodm1  12381  fprod1p  12382  fprodm1s  12384  fprodp1s  12385  fprodunsn  12387  fprodcl2lem  12388  fprodabs  12399  fprodeq0  12400  fprodap0  12404  fprod2dlemstep  12405  fprodcom2fi  12409  fprodrec  12412  fprodmodd  12424  efcvgfsum  12450  dvdsssfz1  12635  bitsfi  12740  bitsinv1  12745  dvdsbnd  12749  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlemle  12801  bezoutlemsup  12802  dfgcd3  12803  dfgcd2  12807  nnwodc  12829  uzwodc  12830  nnwosdc  12832  nninfctlemfo  12833  coprmgcdb  12882  prmdc  12924  isprm5  12937  isprm6  12942  phivalfi  13010  phibndlem  13014  dfphi2  13018  hashdvds  13019  phiprmpw  13020  phimullem  13023  eulerthlemfi  13026  dvdsfi  13037  hashgcdeq  13038  phisum  13039  reumodprminv  13052  pclemdc  13087  pc2dvds  13129  pcz  13131  pcprmpw2  13132  pcmptdvds  13144  pcprod  13145  pcfac  13149  qexpz  13151  prmpwdvds  13154  pockthg  13156  infpnlem2  13159  1arithlem4  13165  1arith  13166  4sqlemafi  13194  4sqlemffi  13195  4sqleminfi  13196  ballotfilemcinfi  13273  ballotfilemdifcfi  13274  ballotfilemcinfz  13275  ballotfilemdifcfz  13276  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemefi  13286  ballotfilemodife  13289  ballotfilemiex  13293  ennnfonelemex  13354  ennnfonelemfun  13357  ennnfonelemf1  13358  ennnfonelemnn0  13362  ennnfonelemim  13364  exmidunben  13366  ctinfomlemom  13367  ctinfom  13368  ctinf  13370  ctiunctlemudc  13377  ctiunctlemf  13378  ctiunctlemfo  13379  omctfn  13383  ssnnctlemct  13386  nninfdclemcl  13388  nninfdclemp1  13390  imasival  13676  ismgmid2  13749  mgmidsssn0  13753  grpinvalem  13754  grpinva  13755  gzsumress  13761  issgrpd  13776  sgrpidmndm  13782  ismndd  13799  mndpfo  13800  mhmima  13847  mhmeql  13848  gsumvallem2  13849  isgrpd2e  13874  dfgrp2  13881  grpidd2  13895  isgrpinv  13908  grplrinv  13911  grpidinv  13913  dfgrp3me  13954  mhmmnd  13968  ghmgrp  13970  mulgsubcl  13988  issubg2m  14041  issubgrpd2  14042  grpissubg  14046  subgintm  14050  nmzsubg  14062  ssnmz  14063  ghmrn  14109  ghmeql  14119  ghmf1  14125  conjnmz  14131  conjnmzb  14132  rinvmod  14162  gsummptfidmadd  14210  prdsplusgsgrpcl  14239  prdsplusgcl  14241  prdsidlem  14242  prdsinvlem  14245  pwsbas  14254  srgrz  14337  srglz  14338  srgisid  14339  ringsrg  14401  rhmdvdsr  14531  rhmopp  14532  subrngintm  14569  subrg1  14588  subrgugrp  14597  subrgintm  14600  rrgsupp  14623  unitrrg  14625  aprap  14647  islmodd  14678  lssuni  14749  lsssubg  14763  lssintclm  14770  dflidl2rng  14867  lidlsubg  14872  cnsubglem  14965  gsumfsum  14972  znf1o  15035  znidomb  15042  asclfnd  15072  psrbagfi  15108  psrbaglecl  15109  psrbagcon  15111  psr1clfi  15128  mplsubgfilemm  15138  mplsubgfilemcl  15139  mplsubgfi  15141  fiinbas  15199  tgclb  15215  restbasg  15318  iscnp4  15368  cnco  15371  cnptopco  15372  cnss1  15376  cnss2  15377  cncnpi  15378  cncnp  15380  cnconst2  15383  cnrest  15385  cnptopresti  15388  cnpdis  15392  lmtopcnp  15400  txbasval  15417  tx1cn  15419  tx2cn  15420  txcnp  15421  upxp  15422  txdis1cn  15428  cnmpt11  15433  psmet0  15477  psmettri2  15478  psmetxrge0  15482  psmetres2  15483  ismeti  15496  xmetpsmet  15519  blsscls2  15643  comet  15649  xmettx  15660  tgioo  15704  tgqioo  15705  fsumcncntop  15717  elcncf1di  15729  cdivcncfap  15754  mulcncflem  15757  mulcncf  15758  cnopnap  15761  divcncfap  15764  dedekindeulemuub  15767  dedekindeulemlu  15771  suplociccreex  15774  suplociccex  15775  dedekindicclemuub  15776  dedekindicclemlu  15780  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemdisj  15790  ivthinclemloc  15791  ivthinc  15793  ivthdec  15794  dich0  15802  ivthdich  15803  cnplimclemr  15819  limccnp2cntop  15827  limccoap  15828  dvcn  15850  dvfre  15860  dvrecap  15863  dvmptclx  15868  dvmptaddx  15869  dvmptmulx  15870  dveflem  15876  dvef  15877  ply1termlem  15892  plyaddlem1  15897  plymullem1  15898  plycoeid3  15907  plycj  15911  plyreres  15914  dvply1  15915  sin0pilem1  15932  sin0pilem2  15933  zprmlogbaplem2  16135  ppiqfi  16158  prmdvdsfi  16159  ppiprm  16170  ppidif  16175  mpodvdsmulf1o  16185  ppiqub  16194  mersenne  16195  perfectlem2  16198  bposlem1  16209  bposlem3  16211  bposlem5  16213  lgsval2lem  16227  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem1f1o  16277  gausslemma2dlem2  16279  gausslemma2dlem3  16280  lgsquadlemofi  16293  lgsquadlem1  16294  lgsquadlem2  16295  2lgslem1a1  16303  2sqlem6  16337  2sqlem8  16340  2sqlem10  16342  usgruspgrben  16525  uspgredg2v  16560  usgredg2v  16563  subuhgr  16611  subupgr  16612  subumgr  16613  subusgr  16614  vtxedgfi  16628  vtxlpfi  16629  wlk1walkdom  16698  wlkres  16718  eupth2lembfi  16816  depindlem1  16845  depindlem2  16846  depindlem3  16847  dichmul0or  16858  fnmptd  16930  bj-charfun  16931  bj-charfundc  16932  bj-charfunr  16934  pw1nct  17131  wexmiddiffi  17142  nnsf  17146  nninfalllem1  17149  nninfall  17150  nninfself  17154  nninfsellemeq  17155  nninfsellemeqinf  17157  nninfsel  17158  nnnninfex  17163  nninfnfiinf  17164  repiecef  17175  isomninnlem  17177  trilpolemeq1  17187  trilpo  17190  apdiff  17195  iswomninnlem  17197  iswomni0  17199  ismkvnnlem  17200  redcwlpo  17203  redc0  17205  reap0  17206  dceqnconst  17208  dcapnconst  17209  nconstwlpolem  17213  nconstwlpo  17214  neapmkv  17216  ltlenmkv  17218