Theorem ralrimiv 2819

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)

Hypothesis

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

Assertion

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

Distinct variable group:   ph, x

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

Proof of Theorem ralrimiv

Step	Hyp	Ref	Expression
1		nfv 1673	. 2 |- F/ x ph
2		ralrimiv.1	. 2 |- ( ph -> ( x e. A -> ps ) )
3	1, 2	ralrimi 2818	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 1756   A.wral 2736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590  df-ral 2741

This theorem is referenced by:  ralrimiva  2820  ralrimivw  2821  ralrimivv  2828  r19.27av  2876  rr19.3v  3122  rabssdv  3453  rzal  3802  trin  4416  class2seteq  4481  ralxfrALT  4532  onmindif  4829  issref  5232  fnprb  5957  fnprOLD  5958  ssorduni  6418  onminex  6439  onmindif2  6444  suceloni  6445  limuni3  6484  frxp  6703  poxp  6705  onfununi  6823  onnseq  6826  tfrlem12  6869  tz7.48-2  6918  oaass  7021  omass  7040  oelim2  7055  oelimcl  7060  oaabs2  7105  omabs  7107  undifixp  7320  dom2lem  7370  isinf  7547  unblem4  7588  unbnn2  7590  marypha1lem  7704  supiso  7743  ordiso2  7750  card2inf  7791  elirrv  7833  wemapwe  7949  wemapweOLD  7950  trcl  7969  tz9.13  8019  rankval3b  8054  rankunb  8078  rankuni2b  8081  scott0  8114  dfac8alem  8220  carduniima  8287  alephsmo  8293  alephval3  8301  iunfictbso  8305  dfac3  8312  dfac5lem5  8318  dfac12r  8336  dfac12k  8337  kmlem4  8343  kmlem11  8350  cfsuc  8447  cofsmo  8459  cfsmolem  8460  coftr  8463  alephsing  8466  infpssrlem3  8495  fin23lem30  8532  isf32lem2  8544  isf32lem3  8545  isf34lem6  8570  fin1a2lem11  8600  fin1a2lem13  8602  fin1a2s  8604  axcc2lem  8626  domtriomlem  8632  axdc3lem2  8641  axdc4lem  8645  axcclem  8647  axdclem2  8710  iundom2g  8725  uniimadom  8729  cardmin  8749  alephval2  8757  alephreg  8767  fpwwe2lem12  8829  wunex2  8926  wuncval2  8935  tskwe2  8961  inar1  8963  tskuni  8971  gruun  8994  intgru  9002  grutsk1  9009  genpcl  9198  ltexprlem5  9230  suplem1pr  9242  supexpr  9244  supsrlem  9299  axpre-sup  9357  supmul1  10316  supmullem1  10317  supmul  10319  peano5nni  10346  uzind  10754  zindd  10764  uzwo  10938  uzwoOLD  10939  lbzbi  10964  xrsupsslem  11290  xrinfmsslem  11291  supxrun  11299  supxrpnf  11302  supxrunb1  11303  supxrunb2  11304  icoshftf1o  11429  flval3  11684  axdc4uzlem  11825  2cshw  12468  cshweqrep  12476  sqrlem1  12753  sqrlem6  12758  fsum0diag2  13271  alzdvds  13604  gcdcllem1  13716  maxprmfct  13820  unbenlem  13990  vdwlem6  14068  vdwlem10  14072  firest  14392  mrieqv2d  14598  iscatd  14632  setcmon  14976  setcepi  14977  isglbd  15308  isacs4lem  15359  acsfiindd  15368  acsmapd  15369  psss  15405  ghmrn  15781  ghmpreima  15789  cntz2ss  15871  symgextres  15951  psgnunilem2  16022  lsmsubg  16174  efgsfo  16257  gsumzaddlem  16429  gsumzaddlemOLD  16431  dmdprdd  16503  dprd2da  16563  imasrng  16733  isabvd  16927  issrngd  16968  islssd  17039  lbsextlem3  17263  lbsextlem4  17264  lidldvgen  17359  psgnghm  18032  isphld  18105  frlmsslsp  18245  frlmsslspOLD  18246  tgcl  18596  distop  18622  indistopon  18627  pptbas  18634  toponmre  18719  opnnei  18746  neiuni  18748  neindisj2  18749  ordtrest2  18830  cnpnei  18890  cnindis  18918  cmpcld  19027  uncmp  19028  hauscmplem  19031  2ndc1stc  19077  1stcrest  19079  1stcelcls  19087  llyrest  19111  nllyrest  19112  cldllycmp  19121  txcls  19199  ptpjcn  19206  ptclsg  19210  dfac14lem  19212  xkoccn  19214  txlly  19231  txnlly  19232  ptrescn  19234  tx1stc  19245  xkoco1cn  19252  xkoco2cn  19253  xkococn  19255  xkoinjcn  19282  qtopeu  19311  hmeofval  19353  ordthmeolem  19396  isfild  19453  fbasrn  19479  trfil2  19482  flimclslem  19579  fclsrest  19619  fclscf  19620  flimfcls  19621  alexsubALTlem1  19641  alexsubALTlem2  19642  alexsubALTlem3  19643  alexsubALT  19645  divstgpopn  19712  isxmetd  19923  imasdsf1olem  19970  blcls  20103  prdsxmslem2  20126  metustfbasOLD  20162  metustfbas  20163  dscmet  20187  nrmmetd  20189  reperflem  20417  reconnlem2  20426  xrge0tsms  20433  fsumcn  20468  cnheibor  20549  tchcph  20774  lmmbr  20791  caubl  20840  ivthlem1  20957  ovolctb  20995  ovoliunlem2  21008  ovolscalem1  21018  ovolicc2  21027  voliunlem3  21055  ismbfd  21140  mbfimaopnlem  21155  itg2le  21239  ellimc2  21374  c1liplem1  21490  plyeq0lem  21700  dgreq0  21754  aannenlem1  21816  pilem2  21939  cxpcn3lem  22207  scvxcvx  22401  musum  22553  dchrisum0flb  22781  ostth2lem2  22905  usgrares1  23345  nbusgra  23361  nbgra0nb  23362  nbgra0edg  23365  cusgrafilem2  23410  usgrasscusgra  23413  uvtxnbgravtx  23425  fargshiftf  23544  fargshiftfva  23547  eupatrl  23611  eupap1  23619  htthlem  24341  ocsh  24708  shintcli  24754  pjss2coi  25590  pjnormssi  25594  pjclem4  25625  pj3si  25633  pj3cor1i  25635  strlem3a  25678  strb  25684  hstrlem3a  25686  hstrbi  25692  spansncv2  25719  mdsl1i  25747  cvmdi  25750  mdexchi  25761  h1da  25775  mdsymlem6  25834  sumdmdii  25841  dmdbr5ati  25848  isoun  26019  supssd  26026  xrge0tsmsd  26275  ordtrest2NEW  26375  pwsiga  26595  measiun  26654  dya2iocuni  26720  erdszelem8  27108  cvmsss2  27185  cvmfolem  27190  rtrclreclem.min  27371  dfrtrcl2  27372  dfon2lem8  27625  dfon2lem9  27626  dfon2  27627  rdgprc  27630  trpredtr  27716  trpredmintr  27717  trpredelss  27718  dftrpred3g  27719  trpredpo  27721  trpredrec  27724  wfrlem15  27760  frr3g  27789  frrlem5b  27795  frrlem5d  27797  sltval2  27819  supaddc  28443  supadd  28444  heicant  28452  mblfinlem1  28454  ftc2nc  28502  nn0prpwlem  28543  ntruni  28548  clsint2  28550  fneint  28575  reftr  28587  fnessref  28591  refssfne  28592  locfincf  28604  comppfsc  28605  neibastop1  28606  neibastop2lem  28607  sdclem2  28664  fdc  28667  seqpo  28669  prdsbnd  28718  heibor  28746  rrnequiv  28760  0idl  28851  intidl  28855  unichnidl  28857  prnc  28893  pellfundre  29248  pellfundge  29249  pellfundlb  29251  dford3lem1  29401  aomclem2  29434  hashgcdeq  29592  addrcom  29757  funressnfv  30060  tz6.12-afv  30105  otiunsndisj  30158  usg2wlkeq  30315  clwwlkn0  30463  clwwisshclwwlem  30496  0egra0rgra  30575  3cyclfrgrarn  30631  vdgn1frgrav3  30647  numclwlk2lem2f1o  30724  frgraregord013  30737  gsummptnn0fzfv  30841  ellcoellss  30966  lindsrng01  30999  snlindsntorlem  31001  mp2pm2mplem4  31134  iunconlem2  31767  bnj518  31975  bnj1137  32082  bnj1136  32084  bnj1413  32122  bnj1417  32128  bnj60  32149  lsmcv2  32770  lcvexchlem4  32778  lcvexchlem5  32779  eqlkr  32840  paddclN  33582  pclfinN  33640  ldilcnv  33855  ldilco  33856  cdleme25dN  34096  cdlemj2  34562  tendocan  34564  erng1lem  34727  erngdvlem4-rN  34739  dihord2pre  34966  dihglblem2N  35035  dochvalr  35098  hdmap14lem12  35623  hdmap14lem13  35624