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	|- ( ( ph /\ x e. A ) -> ps )

Assertion

Ref	Expression
ralrimiva	|- ( ph -> A. x e. A ps )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem ralrimiva

Step	Hyp	Ref	Expression
1		ralrimiva.1	. . 3 |- ( ( ph /\ x e. A ) -> ps )
2	1	ex 115	. 2 |- ( ph -> ( x e. A -> ps ) )
3	2	ralrimiv 2622	1 |- ( ph -> A. x e. A ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   A.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  gsummptfidmsplit  14248  prdsplusgsgrpcl  14281  prdsplusgcl  14283  prdsidlem  14284  prdsinvlem  14287  pwsbas  14296  srgrz  14379  srglz  14380  srgisid  14381  ringsrg  14443  rhmdvdsr  14573  rhmopp  14574  subrngintm  14611  subrg1  14630  subrgugrp  14639  subrgintm  14642  rrgsupp  14665  unitrrg  14667  aprap  14689  islmodd  14720  lssuni  14791  lsssubg  14805  lssintclm  14812  dflidl2rng  14909  lidlsubg  14914  cnsubglem  15007  gsumfsum  15014  znf1o  15077  znidomb  15084  asclfnd  15114  psrbagfi  15150  psrbaglecl  15151  psrbagcon  15153  psrbaglefifi  15154  psr1clfi  15177  psrlidmfi  15178  mplsubgfilemm  15188  mplsubgfilemcl  15189  mplsubgfi  15191  fiinbas  15249  tgclb  15265  restbasg  15368  iscnp4  15418  cnco  15421  cnptopco  15422  cnss1  15426  cnss2  15427  cncnpi  15428  cncnp  15430  cnconst2  15433  cnrest  15435  cnptopresti  15438  cnpdis  15442  lmtopcnp  15450  txbasval  15467  tx1cn  15469  tx2cn  15470  txcnp  15471  upxp  15472  txdis1cn  15478  cnmpt11  15483  psmet0  15527  psmettri2  15528  psmetxrge0  15532  psmetres2  15533  ismeti  15546  xmetpsmet  15569  blsscls2  15693  comet  15699  xmettx  15710  tgioo  15754  tgqioo  15755  fsumcncntop  15767  elcncf1di  15779  cdivcncfap  15804  mulcncflem  15807  mulcncf  15808  cnopnap  15811  divcncfap  15814  dedekindeulemuub  15817  dedekindeulemlu  15821  suplociccreex  15824  suplociccex  15825  dedekindicclemuub  15826  dedekindicclemlu  15830  ivthinclemlopn  15836  ivthinclemlr  15837  ivthinclemuopn  15838  ivthinclemur  15839  ivthinclemdisj  15840  ivthinclemloc  15841  ivthinc  15843  ivthdec  15844  dich0  15852  ivthdich  15853  cnplimclemr  15869  limccnp2cntop  15877  limccoap  15878  dvcn  15900  dvfre  15910  dvrecap  15913  dvmptclx  15918  dvmptaddx  15919  dvmptmulx  15920  dveflem  15926  dvef  15927  ply1termlem  15942  plyaddlem1  15947  plymullem1  15948  plycoeid3  15957  plycj  15961  plyreres  15964  dvply1  15965  sin0pilem1  15982  sin0pilem2  15983  zprmlogbaplem2  16190  ppiqfi  16216  prmdvdsfi  16217  ppiprm  16233  chtprm  16235  chtdif  16238  efchtqdvds  16239  ppidif  16243  prmorcht  16256  mpodvdsmulf1o  16258  ppiqub  16267  chtublem  16269  mersenne  16271  perfectlem2  16274  bposlem1  16285  bposlem3  16287  bposlem5  16289  bposlem6  16290  lgsval2lem  16308  lgsdirnn0  16345  lgsdinn0  16346  gausslemma2dlem1f1o  16358  gausslemma2dlem2  16360  gausslemma2dlem3  16361  lgsquadlemofi  16374  lgsquadlem1  16375  lgsquadlem2  16376  2lgslem1a1  16384  2sqlem6  16418  2sqlem8  16421  2sqlem10  16423  usgruspgrben  16606  uspgredg2v  16641  usgredg2v  16644  subuhgr  16692  subupgr  16693  subumgr  16694  subusgr  16695  vtxedgfi  16709  vtxlpfi  16710  wlk1walkdom  16779  wlkres  16799  eupth2lembfi  16897  depindlem1  16926  depindlem2  16927  depindlem3  16928  dichmul0or  16939  fnmptd  17011  bj-charfun  17012  bj-charfundc  17013  bj-charfunr  17015  pw1nct  17212  wexmiddiffi  17223  nnsf  17227  nninfalllem1  17230  nninfall  17231  nninfself  17235  nninfsellemeq  17236  nninfsellemeqinf  17238  nninfsel  17239  nnnninfex  17244  nninfnfiinf  17245  repiecef  17256  isomninnlem  17258  trilpolemeq1  17269  trilpo  17272  apdiff  17277  iswomninnlem  17279  iswomni0  17281  ismkvnnlem  17282  redcwlpo  17285  redc0  17287  reap0  17288  dceqnconst  17290  dcapnconst  17291  nconstwlpolem  17295  nconstwlpo  17296  neapmkv  17298  ltlenmkv  17300