Theorem ralrimivva 2632

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)

Hypothesis

Ref	Expression
ralrimivva.1	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ps )

Assertion

Ref	Expression
ralrimivva	|- ( ph -> A. x e. A A. y e. B ps )

Distinct variable groups:   ph, x, y   y, A

Allowed substitution hints:   ps( x, y)   A( x)   B( x, y)

Proof of Theorem ralrimivva

Step	Hyp	Ref	Expression
1		ralrimivva.1	. . 3 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ps )
2	1	ex 115	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ps ) )
3	2	ralrimivv 2631	1 |- ( ph -> A. x e. A A. y e. B 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:  swopo  4451  sosng  4848  fcof1  5989  fliftfund  6003  isoresbr  6015  isocnv  6017  f1oiso  6032  oveqrspc2v  6112  caovclg  6242  caovcomg  6245  off  6315  caofrss  6334  caofdig  6336  oprssdmm  6405  dmmpog  6445  fnmpoovd  6451  fmpoco  6452  poxp  6468  f1od2  6471  suppofss1dcl  6504  suppofss2dcl  6505  eroprf  6902  dom2lem  7058  xpf1o  7144  fidifsnid  7173  nnwetri  7223  undiffi  7232  fidcenumlemim  7269  supmoti  7333  supsnti  7345  supisoti  7350  difinfsnlem  7439  nninfwlpor  7514  netap  7620  2omotaplemap  7623  cc2lem  7632  addlocpr  7903  mullocpr  7938  cauappcvgprlemloc  8019  cauappcvgprlemlim  8028  caucvgprlemloc  8042  caucvgprprlemloc  8070  suplocexprlemloc  8088  suplocsrlemb  8173  rereceu  8256  axpre-suploclemres  8268  ltordlem  8810  cju  9291  exbtwnz  10685  frec2uzf1od  10843  frec2uzisod  10844  frecuzrdgrrn  10845  frec2uzrdg  10846  frecuzrdgrcl  10847  frecuzrdgsuc  10851  frecuzrdgrclt  10852  frecuzrdgg  10853  frecuzrdgsuctlem  10860  seqvalcd  10898  seqovcd  10904  seq3caopr3  10928  seq3caopr2  10930  seqcaopr2g  10931  iseqf1olemqf1o  10943  seq3homo  10964  seqhomog  10967  seqfeq4g  10968  seq3distr  10969  fimaxq  11270  zfz1isolem1  11292  wrd2ind  11495  rsqrmo  11793  climcn2  12075  addcn2  12076  mulcn2  12078  fsum2dlemstep  12201  fisumcom2  12205  cvgratnn  12298  fprodcl2lem  12372  fprod2dlemstep  12389  fprodcom2fi  12393  divalglemeunn  12688  divalglemeuneg  12690  bezoutlemeu  12784  isprm6  12925  pw2dvdseu  12946  crth  13002  eulerthlemh  13009  4sqlemffi  13175  ennnfonelemim  13315  nninfdclemf1  13343  unbendc  13345  imasaddfnlemg  13635  ercpbl  13652  plusffng  13685  mgmplusf  13686  opifismgmdc  13691  issgrpd  13727  sgrppropd  13728  ismndd  13750  mndpropd  13753  issubmnd  13755  mndinvmod  13758  mhmpropd  13773  idmhm  13776  mhmf1o  13777  issubmd  13781  mndissubm  13782  submid  13784  0mhm  13793  resmhm  13794  resmhm2  13795  resmhm2b  13796  mhmco  13797  grppropd  13822  grpsubf  13884  dfgrp3m  13904  mhmmnd  13919  mhmfmhm  13920  mulgfng  13927  issubg4m  13996  grpissubg  13997  isnsg3  14010  0nsg  14017  nsgid  14018  isghmd  14055  ghmmhm  14056  idghm  14062  ghmnsgima  14071  ghmnsgpreima  14072  ghmf1  14076  kerf1ghm  14077  ghmf1o  14078  cmnsubm  14112  ghmcmn  14131  invghm  14133  ablnsg  14138  imasabl  14140  srgfcl  14277  srglmhm  14297  srgrmhm  14298  isrhm2d  14472  subrngringnsg  14513  issubrng2  14518  subrngintm  14520  issubrg2  14549  subrgintm  14551  aprap  14598  aprlring  14600  islmodd  14629  lmodscaf  14647  lmodprop2d  14685  islssmd  14696  islss4  14719  lsspropdg  14768  issubrgd  14789  dflidl2rng  14818  rnglidlmmgm  14833  expghmap  14942  mulgghm2  14943  znf1o  14986  znidom  14992  issubassa2  15035  tgclb  15166  txbas  15359  txcnp  15372  txcnmpt  15374  cnmpt21  15392  txswaphmeo  15422  isxmetd  15448  isxmet2d  15449  xmettpos  15471  blfvalps  15486  xmetresbl  15541  metss2  15599  comet  15600  bdmet  15603  bdmopn  15605  xmetxp  15608  qtopbasss  15622  elcncf1di  15680  cncfcdm  15683  mulc1cncf  15690  cncfco  15692  dedekindeulemloc  15720  dedekindeu  15724  dedekindicclemloc  15729  dedekindicclemicc  15733  ivthinclemloc  15742  dich0  15753  dvmptfsum  15826  mpodvdsmulf1o  16104  fsumdvdsmul  16105  gausslemma2dlem1f1o  16179  lgseisenlem2  16190  lgsquadlemsfi  16194  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  usgredgreu  16457  uspgredg2vtxeu  16459  uspgredg2v  16462  usgredg2v  16465  vtxedgfi  16530  vtxlpfi  16531  dichmul0or  16760  sssneq  17032  exmidsbthrlem  17067  cvgcmp2n  17082  trirec0  17093  apdiff  17097  redc0  17107  reap0  17108  cndcap  17109  neap0mkv  17119