Theorem ralrimivva 2612

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  swopo  4397  sosng  4792  fcof1  5913  fliftfund  5927  isoresbr  5939  isocnv  5941  f1oiso  5956  oveqrspc2v  6034  caovclg  6164  caovcomg  6167  off  6237  caofrss  6256  caofdig  6258  oprssdmm  6323  dmmpog  6361  fnmpoovd  6367  fmpoco  6368  poxp  6384  f1od2  6387  eroprf  6783  dom2lem  6931  xpf1o  7013  fidifsnid  7041  nnwetri  7086  undiffi  7095  fidcenumlemim  7127  supmoti  7168  supsnti  7180  supisoti  7185  difinfsnlem  7274  nninfwlpor  7349  netap  7448  2omotaplemap  7451  cc2lem  7460  addlocpr  7731  mullocpr  7766  cauappcvgprlemloc  7847  cauappcvgprlemlim  7856  caucvgprlemloc  7870  caucvgprprlemloc  7898  suplocexprlemloc  7916  suplocsrlemb  8001  rereceu  8084  axpre-suploclemres  8096  ltordlem  8637  cju  9116  exbtwnz  10478  frec2uzf1od  10636  frec2uzisod  10637  frecuzrdgrrn  10638  frec2uzrdg  10639  frecuzrdgrcl  10640  frecuzrdgsuc  10644  frecuzrdgrclt  10645  frecuzrdgg  10646  frecuzrdgsuctlem  10653  seqvalcd  10691  seqovcd  10697  seq3caopr3  10721  seq3caopr2  10723  seqcaopr2g  10724  iseqf1olemqf1o  10736  seq3homo  10757  seqhomog  10760  seqfeq4g  10761  seq3distr  10762  fimaxq  11057  zfz1isolem1  11070  wrd2ind  11263  rsqrmo  11546  climcn2  11828  addcn2  11829  mulcn2  11831  fsum2dlemstep  11953  fisumcom2  11957  cvgratnn  12050  fprodcl2lem  12124  fprod2dlemstep  12141  fprodcom2fi  12145  divalglemeunn  12440  divalglemeuneg  12442  bezoutlemeu  12536  isprm6  12677  pw2dvdseu  12698  crth  12754  eulerthlemh  12761  4sqlemffi  12927  ennnfonelemim  13003  nninfdclemf1  13031  unbendc  13033  imasaddfnlemg  13355  ercpbl  13372  plusffng  13406  mgmplusf  13407  opifismgmdc  13412  issgrpd  13453  sgrppropd  13454  ismndd  13478  mndpropd  13481  issubmnd  13483  mndinvmod  13486  mhmpropd  13507  idmhm  13510  mhmf1o  13511  issubmd  13515  mndissubm  13516  submid  13518  0mhm  13527  resmhm  13528  resmhm2  13529  resmhm2b  13530  mhmco  13531  grppropd  13558  grpsubf  13620  dfgrp3m  13640  mhmmnd  13661  mhmfmhm  13662  mulgfng  13669  issubg4m  13738  grpissubg  13739  isnsg3  13752  0nsg  13759  nsgid  13760  isghmd  13797  ghmmhm  13798  idghm  13804  ghmnsgima  13813  ghmnsgpreima  13814  ghmf1  13818  kerf1ghm  13819  ghmf1o  13820  ghmcmn  13872  invghm  13874  ablnsg  13879  imasabl  13881  srgfcl  13944  srglmhm  13964  srgrmhm  13965  isrhm2d  14137  subrngringnsg  14177  issubrng2  14182  subrngintm  14184  issubrg2  14213  subrgintm  14215  aprap  14258  islmodd  14265  lmodscaf  14282  lmodprop2d  14320  islssmd  14331  islss4  14354  lsspropdg  14403  issubrgd  14424  dflidl2rng  14453  rnglidlmmgm  14468  expghmap  14579  mulgghm2  14580  znf1o  14623  znidom  14629  tgclb  14747  txbas  14940  txcnp  14953  txcnmpt  14955  cnmpt21  14973  txswaphmeo  15003  isxmetd  15029  isxmet2d  15030  xmettpos  15052  blfvalps  15067  xmetresbl  15122  metss2  15180  comet  15181  bdmet  15184  bdmopn  15186  xmetxp  15189  qtopbasss  15203  elcncf1di  15261  cncfcdm  15264  mulc1cncf  15271  cncfco  15273  dedekindeulemloc  15301  dedekindeu  15305  dedekindicclemloc  15310  dedekindicclemicc  15314  ivthinclemloc  15323  dich0  15334  dvmptfsum  15407  mpodvdsmulf1o  15672  fsumdvdsmul  15673  gausslemma2dlem1f1o  15747  lgseisenlem2  15758  lgsquadlemsfi  15762  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  usgredgreu  16022  uspgredg2vtxeu  16024  uspgredg2v  16027  usgredg2v  16030  sssneq  16394  exmidsbthrlem  16417  cvgcmp2n  16428  trirec0  16439  apdiff  16443  redc0  16452  reap0  16453  cndcap  16454  neap0mkv  16464