Theorem ralrimivva 2576

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 2575	1 |- ( ph -> A. x e. A A. y e. B ps )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2164   A.wral 2472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  swopo  4337  sosng  4732  fcof1  5826  fliftfund  5840  isoresbr  5852  isocnv  5854  f1oiso  5869  oveqrspc2v  5945  caovclg  6071  caovcomg  6074  off  6143  caofrss  6157  caofdig  6159  oprssdmm  6224  dmmpog  6262  fnmpoovd  6268  fmpoco  6269  poxp  6285  f1od2  6288  eroprf  6682  dom2lem  6826  xpf1o  6900  fidifsnid  6927  nnwetri  6972  undiffi  6981  fidcenumlemim  7011  supmoti  7052  supsnti  7064  supisoti  7069  difinfsnlem  7158  nninfwlpor  7233  netap  7314  2omotaplemap  7317  cc2lem  7326  addlocpr  7596  mullocpr  7631  cauappcvgprlemloc  7712  cauappcvgprlemlim  7721  caucvgprlemloc  7735  caucvgprprlemloc  7763  suplocexprlemloc  7781  suplocsrlemb  7866  rereceu  7949  axpre-suploclemres  7961  ltordlem  8501  cju  8980  exbtwnz  10319  frec2uzf1od  10477  frec2uzisod  10478  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgg  10487  frecuzrdgsuctlem  10494  seqvalcd  10532  seqovcd  10538  seq3caopr3  10562  seq3caopr2  10564  seqcaopr2g  10565  iseqf1olemqf1o  10577  seq3homo  10598  seqhomog  10601  seqfeq4g  10602  seq3distr  10603  fimaxq  10898  zfz1isolem1  10911  rsqrmo  11171  climcn2  11452  addcn2  11453  mulcn2  11455  fsum2dlemstep  11577  fisumcom2  11581  cvgratnn  11674  fprodcl2lem  11748  fprod2dlemstep  11765  fprodcom2fi  11769  divalglemeunn  12062  divalglemeuneg  12064  bezoutlemeu  12144  isprm6  12285  pw2dvdseu  12306  crth  12362  eulerthlemh  12369  4sqlemffi  12534  ennnfonelemim  12581  nninfdclemf1  12609  unbendc  12611  imasaddfnlemg  12897  ercpbl  12914  plusffng  12948  mgmplusf  12949  opifismgmdc  12954  issgrpd  12995  sgrppropd  12996  ismndd  13018  mndpropd  13021  issubmnd  13023  mndinvmod  13026  mhmpropd  13038  idmhm  13041  mhmf1o  13042  issubmd  13046  mndissubm  13047  submid  13049  0mhm  13058  resmhm  13059  resmhm2  13060  resmhm2b  13061  mhmco  13062  grppropd  13089  grpsubf  13151  dfgrp3m  13171  mhmmnd  13186  mhmfmhm  13187  mulgfng  13194  issubg4m  13263  grpissubg  13264  isnsg3  13277  0nsg  13284  nsgid  13285  isghmd  13322  ghmmhm  13323  idghm  13329  ghmnsgima  13338  ghmnsgpreima  13339  ghmf1  13343  kerf1ghm  13344  ghmf1o  13345  ghmcmn  13397  invghm  13399  ablnsg  13404  imasabl  13406  srgfcl  13469  srglmhm  13489  srgrmhm  13490  isrhm2d  13661  subrngringnsg  13701  issubrng2  13706  subrngintm  13708  issubrg2  13737  subrgintm  13739  aprap  13782  islmodd  13789  lmodscaf  13806  lmodprop2d  13844  islssmd  13855  islss4  13878  lsspropdg  13927  issubrgd  13948  dflidl2rng  13977  rnglidlmmgm  13992  expghmap  14095  mulgghm2  14096  znf1o  14139  znidom  14145  tgclb  14233  txbas  14426  txcnp  14439  txcnmpt  14441  cnmpt21  14459  txswaphmeo  14489  isxmetd  14515  isxmet2d  14516  xmettpos  14538  blfvalps  14553  xmetresbl  14608  metss2  14666  comet  14667  bdmet  14670  bdmopn  14672  xmetxp  14675  qtopbasss  14689  elcncf1di  14734  cncfcdm  14737  mulc1cncf  14744  cncfco  14746  dedekindeulemloc  14773  dedekindeu  14777  dedekindicclemloc  14782  dedekindicclemicc  14786  ivthinclemloc  14795  dich0  14806  gausslemma2dlem1f1o  15176  lgseisenlem2  15187  lgsquadlem1  15191  sssneq  15492  exmidsbthrlem  15512  cvgcmp2n  15523  trirec0  15534  apdiff  15538  redc0  15547  reap0  15548  cndcap  15549  neap0mkv  15559