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  4213  triun  4244  issod  4466  frirrg  4497  frind  4499  peano2  4744  dmmptd  5517  fun11iun  5663  fniinfv  5764  eqfnfv  5809  eqfnfvd  5812  fnmptfvd  5816  dff3im  5856  dffo4  5859  fmptd  5865  ffnfv  5869  fmpt2d  5873  ffvresb  5874  funiun  5893  fconst2g  5933  fconstfvm  5936  resfunexg  5939  eufnfv  5952  foco2  5962  fniunfv  5971  fcofo  5993  fliftel  6002  fliftfun  6005  fliftfuns  6007  riota5f  6068  f1ocnvd  6295  f1o3d  6301  suppssov1  6302  offval2  6322  ofrfval2  6323  offveqb  6326  offveq  6327  caofref  6331  caofinvl  6332  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  opabex3d  6354  uchoice  6375  oprssdmm  6409  f1od2  6475  disjxp1  6476  funsssuppss  6502  suppofss1dcl  6508  suppofss2dcl  6509  tfrlem1  6583  tfrlemisucaccv  6600  tfrlemiubacc  6605  tfr1onlemsucfn  6615  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemubacc  6621  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllemsucfn  6628  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemubacc  6634  tfrcllemaccex  6636  tfrcllemres  6637  tfrcl  6639  rdgon  6661  freccllem  6677  frecfcllem  6679  omcl  6738  oeicl  6739  qliftfuns  6897  ixpeq2dva  6999  xpf1o  7148  mapxpen  7152  isinfinf  7205  fimax2gtrilemstep  7209  undifdcss  7234  opabfi  7251  fissfi  7267  relresfin  7268  fdcf1  7321  f1setfi  7322  2omap  7324  eqsuptid  7343  eqinftid  7367  difinfsnlem  7445  difinfsn  7446  ctmlemr  7454  ctm  7455  ctssdclemn0  7456  ctssdccl  7457  enumctlemm  7460  nninfninc  7469  nnnninf  7472  nnnninfeq  7474  enomnilem  7484  ismkvnex  7501  enmkvlem  7507  enwomnilem  7515  nninfwlporlemd  7518  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  nninfwlpoim  7525  nninfinfwlpo  7526  finacn  7566  acfun  7569  exmidaclem  7570  exmidontriimlem4  7586  exmidontriim  7587  pw1on  7591  ccfunen  7636  cc2lem  7638  cc3  7640  acnccim  7644  genprndl  7894  genprndu  7895  nqprloc  7918  ltexprlemrnd  7978  ltexprlemdisj  7979  lteupri  7990  recexprlemrnd  8002  recexprlemdisj  8003  caucvgprlemlim  8054  caucvgprprlemlim  8084  suplocexprlemml  8089  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  caucvgsrlembound  8167  caucvgsrlemgt1  8168  caucvgsrlemoffgt1  8172  caucvgsr  8175  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  elrealeu  8202  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  negeu  8524  eqord1  8818  eqord2  8819  creur  9297  creui  9298  suprzclex  9755  supinfneg  10011  infsupneg  10012  infregelbex  10014  indstr2  10025  irraddap  10063  iooidg  10328  iccsupr  10385  icoshftf1o  10410  fznlem  10462  exfzdc  10676  zsupcllemstep  10679  infssuzex  10683  suprzubdc  10688  zsupssdc  10690  exbtwnzlemstep  10699  exbtwnzlemex  10701  frec2uzrdg  10867  frecuzrdgrcl  10868  frecuzrdgtcl  10870  frecuzrdgsuc  10872  frecuzrdgrclt  10873  frecuzrdgg  10874  frecuzrdgfunlem  10877  frecuzrdgsuctlem  10881  nninfinf  10901  iseqovex  10916  seq3val  10918  seqvalcd  10919  seq3-1  10920  seqf  10922  seq3p1  10923  seqovcd  10925  seqp1cd  10928  seq3clss  10929  seq3fveq2  10933  seqfveq2g  10935  seqfveqg  10936  seq3fveq  10937  seq3feq  10938  seq3shft2  10939  seqshft2g  10940  monoord  10943  monoord2  10944  ser3mono  10945  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seqcaopr3g  10950  seq3caopr2  10951  seqcaopr2g  10952  iseqf1olemqk  10965  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  iseqf1olemfvp  10968  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  seq3f1oleml  10974  seq3f1o  10975  seqf1og  10979  seq3id3  10982  seq3id  10983  seq3id2  10984  seq3homo  10985  seq3z  10986  seqhomog  10988  seqfeq4g  10989  ser3ge0  10994  nn0ltexp2  11169  bccl  11227  hashinfuni  11238  hashennnuni  11240  sshashneg  11303  hashfibclem  11304  hashf1lem1  11307  wrdexg  11337  ccatlen  11385  ccatvalfn  11391  ccatrn  11399  swrdlen  11446  swrdwrdsymbg  11458  swrdswrd  11499  wrdind  11516  reuccatpfxs1  11541  shftf  11617  seq3shft  11625  caucvgrelemcau  11768  cvg1nlemcau  11772  cvg1nlemres  11773  resqrexlemcvg  11807  resqrexlemglsq  11810  resqrexlemga  11811  maxabslemval  11997  negfi  12017  minmax  12020  xrmaxiflemval  12041  xrminmax  12056  climconst  12081  2clim  12092  climcn1  12099  climcn2  12100  reccn2ap  12104  cn1lem  12105  climsqz  12126  climsqz2  12127  climcau  12138  climrecvg1n  12139  serf0  12143  sumeq2dv  12159  sumrbdclem  12169  fsum3cvg  12170  summodclem3  12172  summodclem2a  12173  zsumdc  12176  isum  12177  fsumgcl  12178  fsum3  12179  fsumf1o  12182  isumss  12183  fisumss  12184  isumss2  12185  fsum3cvg2  12186  fsumsersdc  12187  fsum3ser  12189  fsumcl2lem  12190  fsumadd  12198  fsumsplit  12199  fsumm1  12208  fsum1p  12210  isumclim3  12215  isummulc2  12218  sumsplitdc  12224  fsum2dlemstep  12226  fisumcom2  12230  fsumshftm  12237  fsummulc2  12240  fsumge1  12253  fsum00  12254  fsumabs  12257  telfsumo  12258  telfsumo2  12259  fsumparts  12262  fsumrelem  12263  fsumiun  12269  hashiun  12270  hash2iun  12271  binomlem  12275  isumshft  12282  isum1p  12284  isumnn0nn  12285  isumrpcl  12286  isumlessdc  12288  divcnv  12289  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemseq  12318  cvgratnnlemabsle  12319  cvgratnnlemfm  12321  cvgratnnlemrate  12322  cvgratnn  12323  cvgratz  12324  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  clim2prod  12331  prodeq2dv  12358  prodrbdclem  12363  fproddccvg  12364  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  iprodap  12372  fprodseq  12375  fprodf1o  12380  prodssdc  12381  fprodssdc  12382  fprodmul  12383  fprodsplit  12389  fprodm1  12390  fprod1p  12391  fprodm1s  12393  fprodp1s  12394  fprodunsn  12396  fprodcl2lem  12397  fprodabs  12408  fprodeq0  12409  fprodap0  12413  fprod2dlemstep  12414  fprodcom2fi  12418  fprodrec  12421  fprodmodd  12433  efcvgfsum  12459  dvdsssfz1  12644  bitsfi  12749  bitsinv1  12754  dvdsbnd  12758  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlemle  12810  bezoutlemsup  12811  dfgcd3  12812  dfgcd2  12816  nnwodc  12838  uzwodc  12839  nnwosdc  12841  nninfctlemfo  12842  coprmgcdb  12891  prmdc  12933  isprm5  12946  isprm6  12951  phivalfi  13019  phibndlem  13023  dfphi2  13027  hashdvds  13028  phiprmpw  13029  phimullem  13032  eulerthlemfi  13035  dvdsfi  13046  hashgcdeq  13047  phisum  13048  reumodprminv  13061  pclemdc  13096  pc2dvds  13138  pcz  13140  pcprmpw2  13141  pcmptdvds  13153  pcprod  13154  pcfac  13158  qexpz  13160  prmpwdvds  13163  pockthg  13165  infpnlem2  13168  1arithlem4  13174  1arith  13175  4sqlemafi  13203  4sqlemffi  13204  4sqleminfi  13205  ballotfilemcinfi  13282  ballotfilemdifcfi  13283  ballotfilemcinfz  13284  ballotfilemdifcfz  13285  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemefi  13295  ballotfilemodife  13298  ballotfilemiex  13302  ennnfonelemex  13363  ennnfonelemfun  13366  ennnfonelemf1  13367  ennnfonelemnn0  13371  ennnfonelemim  13373  exmidunben  13375  ctinfomlemom  13376  ctinfom  13377  ctinf  13379  ctiunctlemudc  13386  ctiunctlemf  13387  ctiunctlemfo  13388  omctfn  13392  ssnnctlemct  13395  nninfdclemcl  13397  nninfdclemp1  13399  imasival  13686  ismgmid2  13759  mgmidsssn0  13763  grpinvalem  13764  grpinva  13765  gzsumress  13771  issgrpd  13786  sgrpidmndm  13792  ismndd  13809  mndpfo  13810  mhmima  13857  mhmeql  13858  gsumvallem2  13859  isgrpd2e  13884  dfgrp2  13891  grpidd2  13905  isgrpinv  13918  grplrinv  13921  grpidinv  13923  dfgrp3me  13964  mhmmnd  13978  ghmgrp  13980  mulgsubcl  13998  issubg2m  14051  issubgrpd2  14052  grpissubg  14056  subgintm  14060  nmzsubg  14072  ssnmz  14073  ghmrn  14119  ghmeql  14129  ghmf1  14135  conjnmz  14141  conjnmzb  14142  cntzsgrpcl  14167  cntz2ss  14168  cntzsubm  14170  cntzsubg  14171  cntzmhm  14173  cntzmhm2  14174  rinvmod  14203  gsummptfidmadd  14251  gsummptfidmsplit  14254  idjufi  14269  idjusnfi  14270  gsum2dfilem2  14272  gsum2dfi  14273  gsum2d2fi  14274  prdsplusgsgrpcl  14297  prdsplusgcl  14299  prdsidlem  14300  prdsinvlem  14303  pwsbas  14312  srgrz  14395  srglz  14396  srgisid  14397  ringsrg  14459  rhmdvdsr  14591  rhmopp  14592  subrngintm  14629  subrg1  14648  subrgugrp  14657  subrgintm  14660  rrgsupp  14683  unitrrg  14685  aprap  14707  islmodd  14738  lssuni  14809  lsssubg  14823  lssintclm  14830  dflidl2rng  14927  lidlsubg  14932  cnsubglem  15025  gsumfsum  15032  znf1o  15095  znidomb  15102  asclfnd  15132  psrbagfi  15168  psrbaglecl  15169  psrbagcon  15171  psrbaglefifi  15172  psr1clfi  15198  psrlidmfi  15199  psrridmfi  15200  mplsubgfilemm  15214  mplsubgfilemcl  15215  mplsubgfi  15217  fiinbas  15275  tgclb  15291  restbasg  15394  iscnp4  15444  cnco  15447  cnptopco  15448  cnss1  15452  cnss2  15453  cncnpi  15454  cncnp  15456  cnconst2  15459  cnrest  15461  cnptopresti  15464  cnpdis  15468  lmtopcnp  15476  txbasval  15493  tx1cn  15495  tx2cn  15496  txcnp  15497  upxp  15498  txdis1cn  15504  cnmpt11  15509  psmet0  15553  psmettri2  15554  psmetxrge0  15558  psmetres2  15559  ismeti  15572  xmetpsmet  15595  blsscls2  15719  comet  15725  xmettx  15736  tgioo  15780  tgqioo  15781  fsumcncntop  15793  elcncf1di  15805  cdivcncfap  15830  mulcncflem  15833  mulcncf  15834  cnopnap  15837  divcncfap  15840  dedekindeulemuub  15843  dedekindeulemlu  15847  suplociccreex  15850  suplociccex  15851  dedekindicclemuub  15852  dedekindicclemlu  15856  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemdisj  15866  ivthinclemloc  15867  ivthinc  15869  ivthdec  15870  dich0  15878  ivthdich  15879  cnplimclemr  15895  limccnp2cntop  15903  limccoap  15904  dvcn  15926  dvfre  15936  dvrecap  15939  dvmptclx  15944  dvmptaddx  15945  dvmptmulx  15946  dveflem  15952  dvef  15953  ply1termlem  15968  plyaddlem1  15973  plymullem1  15974  plycoeid3  15983  plycj  15987  plyreres  15990  dvply1  15991  sin0pilem1  16008  sin0pilem2  16009  zprmlogbaplem2  16216  ppiqfi  16242  prmdvdsfi  16243  ppiprm  16259  chtprm  16261  chtdif  16264  efchtqdvds  16265  ppidif  16269  prmorcht  16282  mpodvdsmulf1o  16284  ppiqub  16293  chtublem  16295  mersenne  16297  perfectlem2  16300  bposlem1  16311  bposlem3  16313  bposlem5  16315  bposlem6  16316  lgsval2lem  16334  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem1f1o  16384  gausslemma2dlem2  16386  gausslemma2dlem3  16387  lgsquadlemofi  16400  lgsquadlem1  16401  lgsquadlem2  16402  2lgslem1a1  16410  2sqlem6  16444  2sqlem8  16447  2sqlem10  16449  usgruspgrben  16632  uspgredg2v  16667  usgredg2v  16670  subuhgr  16718  subupgr  16719  subumgr  16720  subusgr  16721  vtxedgfi  16735  vtxlpfi  16736  wlk1walkdom  16805  wlkres  16825  eupth2lembfi  16923  depindlem1  16952  depindlem2  16953  depindlem3  16954  dichmul0or  16965  fnmptd  17037  bj-charfun  17038  bj-charfundc  17039  bj-charfunr  17041  pw1nct  17238  wexmiddiffi  17249  nnsf  17254  nninfalllem1  17257  nninfall  17258  nninfself  17262  nninfsellemeq  17263  nninfsellemeqinf  17265  nninfsel  17266  nnnninfex  17271  nninfnfiinf  17272  repiecef  17283  isomninnlem  17285  trilpolemeq1  17296  trilpo  17299  apdiff  17304  iswomninnlem  17306  iswomni0  17308  ismkvnnlem  17309  redcwlpo  17312  redc0  17314  reap0  17315  dceqnconst  17317  dcapnconst  17318  nconstwlpolem  17322  nconstwlpo  17323  neapmkv  17325  ltlenmkv  17327