Theorem ralrimivva 2579

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  swopo  4341  sosng  4736  fcof1  5830  fliftfund  5844  isoresbr  5856  isocnv  5858  f1oiso  5873  oveqrspc2v  5949  caovclg  6076  caovcomg  6079  off  6148  caofrss  6162  caofdig  6164  oprssdmm  6229  dmmpog  6267  fnmpoovd  6273  fmpoco  6274  poxp  6290  f1od2  6293  eroprf  6687  dom2lem  6831  xpf1o  6905  fidifsnid  6932  nnwetri  6977  undiffi  6986  fidcenumlemim  7018  supmoti  7059  supsnti  7071  supisoti  7076  difinfsnlem  7165  nninfwlpor  7240  netap  7321  2omotaplemap  7324  cc2lem  7333  addlocpr  7603  mullocpr  7638  cauappcvgprlemloc  7719  cauappcvgprlemlim  7728  caucvgprlemloc  7742  caucvgprprlemloc  7770  suplocexprlemloc  7788  suplocsrlemb  7873  rereceu  7956  axpre-suploclemres  7968  ltordlem  8509  cju  8988  exbtwnz  10340  frec2uzf1od  10498  frec2uzisod  10499  frecuzrdgrrn  10500  frec2uzrdg  10501  frecuzrdgrcl  10502  frecuzrdgsuc  10506  frecuzrdgrclt  10507  frecuzrdgg  10508  frecuzrdgsuctlem  10515  seqvalcd  10553  seqovcd  10559  seq3caopr3  10583  seq3caopr2  10585  seqcaopr2g  10586  iseqf1olemqf1o  10598  seq3homo  10619  seqhomog  10622  seqfeq4g  10623  seq3distr  10624  fimaxq  10919  zfz1isolem1  10932  rsqrmo  11192  climcn2  11474  addcn2  11475  mulcn2  11477  fsum2dlemstep  11599  fisumcom2  11603  cvgratnn  11696  fprodcl2lem  11770  fprod2dlemstep  11787  fprodcom2fi  11791  divalglemeunn  12086  divalglemeuneg  12088  bezoutlemeu  12174  isprm6  12315  pw2dvdseu  12336  crth  12392  eulerthlemh  12399  4sqlemffi  12565  ennnfonelemim  12641  nninfdclemf1  12669  unbendc  12671  imasaddfnlemg  12957  ercpbl  12974  plusffng  13008  mgmplusf  13009  opifismgmdc  13014  issgrpd  13055  sgrppropd  13056  ismndd  13078  mndpropd  13081  issubmnd  13083  mndinvmod  13086  mhmpropd  13098  idmhm  13101  mhmf1o  13102  issubmd  13106  mndissubm  13107  submid  13109  0mhm  13118  resmhm  13119  resmhm2  13120  resmhm2b  13121  mhmco  13122  grppropd  13149  grpsubf  13211  dfgrp3m  13231  mhmmnd  13246  mhmfmhm  13247  mulgfng  13254  issubg4m  13323  grpissubg  13324  isnsg3  13337  0nsg  13344  nsgid  13345  isghmd  13382  ghmmhm  13383  idghm  13389  ghmnsgima  13398  ghmnsgpreima  13399  ghmf1  13403  kerf1ghm  13404  ghmf1o  13405  ghmcmn  13457  invghm  13459  ablnsg  13464  imasabl  13466  srgfcl  13529  srglmhm  13549  srgrmhm  13550  isrhm2d  13721  subrngringnsg  13761  issubrng2  13766  subrngintm  13768  issubrg2  13797  subrgintm  13799  aprap  13842  islmodd  13849  lmodscaf  13866  lmodprop2d  13904  islssmd  13915  islss4  13938  lsspropdg  13987  issubrgd  14008  dflidl2rng  14037  rnglidlmmgm  14052  expghmap  14163  mulgghm2  14164  znf1o  14207  znidom  14213  tgclb  14301  txbas  14494  txcnp  14507  txcnmpt  14509  cnmpt21  14527  txswaphmeo  14557  isxmetd  14583  isxmet2d  14584  xmettpos  14606  blfvalps  14621  xmetresbl  14676  metss2  14734  comet  14735  bdmet  14738  bdmopn  14740  xmetxp  14743  qtopbasss  14757  elcncf1di  14815  cncfcdm  14818  mulc1cncf  14825  cncfco  14827  dedekindeulemloc  14855  dedekindeu  14859  dedekindicclemloc  14864  dedekindicclemicc  14868  ivthinclemloc  14877  dich0  14888  dvmptfsum  14961  mpodvdsmulf1o  15226  fsumdvdsmul  15227  gausslemma2dlem1f1o  15301  lgseisenlem2  15312  lgsquadlemsfi  15316  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  sssneq  15646  exmidsbthrlem  15666  cvgcmp2n  15677  trirec0  15688  apdiff  15692  redc0  15701  reap0  15702  cndcap  15703  neap0mkv  15713