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  4342  sosng  4737  fcof1  5833  fliftfund  5847  isoresbr  5859  isocnv  5861  f1oiso  5876  oveqrspc2v  5952  caovclg  6080  caovcomg  6083  off  6152  caofrss  6171  caofdig  6173  oprssdmm  6238  dmmpog  6276  fnmpoovd  6282  fmpoco  6283  poxp  6299  f1od2  6302  eroprf  6696  dom2lem  6840  xpf1o  6914  fidifsnid  6941  nnwetri  6986  undiffi  6995  fidcenumlemim  7027  supmoti  7068  supsnti  7080  supisoti  7085  difinfsnlem  7174  nninfwlpor  7249  netap  7337  2omotaplemap  7340  cc2lem  7349  addlocpr  7620  mullocpr  7655  cauappcvgprlemloc  7736  cauappcvgprlemlim  7745  caucvgprlemloc  7759  caucvgprprlemloc  7787  suplocexprlemloc  7805  suplocsrlemb  7890  rereceu  7973  axpre-suploclemres  7985  ltordlem  8526  cju  9005  exbtwnz  10357  frec2uzf1od  10515  frec2uzisod  10516  frecuzrdgrrn  10517  frec2uzrdg  10518  frecuzrdgrcl  10519  frecuzrdgsuc  10523  frecuzrdgrclt  10524  frecuzrdgg  10525  frecuzrdgsuctlem  10532  seqvalcd  10570  seqovcd  10576  seq3caopr3  10600  seq3caopr2  10602  seqcaopr2g  10603  iseqf1olemqf1o  10615  seq3homo  10636  seqhomog  10639  seqfeq4g  10640  seq3distr  10641  fimaxq  10936  zfz1isolem1  10949  rsqrmo  11209  climcn2  11491  addcn2  11492  mulcn2  11494  fsum2dlemstep  11616  fisumcom2  11620  cvgratnn  11713  fprodcl2lem  11787  fprod2dlemstep  11804  fprodcom2fi  11808  divalglemeunn  12103  divalglemeuneg  12105  bezoutlemeu  12199  isprm6  12340  pw2dvdseu  12361  crth  12417  eulerthlemh  12424  4sqlemffi  12590  ennnfonelemim  12666  nninfdclemf1  12694  unbendc  12696  imasaddfnlemg  13016  ercpbl  13033  plusffng  13067  mgmplusf  13068  opifismgmdc  13073  issgrpd  13114  sgrppropd  13115  ismndd  13139  mndpropd  13142  issubmnd  13144  mndinvmod  13147  mhmpropd  13168  idmhm  13171  mhmf1o  13172  issubmd  13176  mndissubm  13177  submid  13179  0mhm  13188  resmhm  13189  resmhm2  13190  resmhm2b  13191  mhmco  13192  grppropd  13219  grpsubf  13281  dfgrp3m  13301  mhmmnd  13322  mhmfmhm  13323  mulgfng  13330  issubg4m  13399  grpissubg  13400  isnsg3  13413  0nsg  13420  nsgid  13421  isghmd  13458  ghmmhm  13459  idghm  13465  ghmnsgima  13474  ghmnsgpreima  13475  ghmf1  13479  kerf1ghm  13480  ghmf1o  13481  ghmcmn  13533  invghm  13535  ablnsg  13540  imasabl  13542  srgfcl  13605  srglmhm  13625  srgrmhm  13626  isrhm2d  13797  subrngringnsg  13837  issubrng2  13842  subrngintm  13844  issubrg2  13873  subrgintm  13875  aprap  13918  islmodd  13925  lmodscaf  13942  lmodprop2d  13980  islssmd  13991  islss4  14014  lsspropdg  14063  issubrgd  14084  dflidl2rng  14113  rnglidlmmgm  14128  expghmap  14239  mulgghm2  14240  znf1o  14283  znidom  14289  tgclb  14385  txbas  14578  txcnp  14591  txcnmpt  14593  cnmpt21  14611  txswaphmeo  14641  isxmetd  14667  isxmet2d  14668  xmettpos  14690  blfvalps  14705  xmetresbl  14760  metss2  14818  comet  14819  bdmet  14822  bdmopn  14824  xmetxp  14827  qtopbasss  14841  elcncf1di  14899  cncfcdm  14902  mulc1cncf  14909  cncfco  14911  dedekindeulemloc  14939  dedekindeu  14943  dedekindicclemloc  14948  dedekindicclemicc  14952  ivthinclemloc  14961  dich0  14972  dvmptfsum  15045  mpodvdsmulf1o  15310  fsumdvdsmul  15311  gausslemma2dlem1f1o  15385  lgseisenlem2  15396  lgsquadlemsfi  15400  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  sssneq  15733  exmidsbthrlem  15753  cvgcmp2n  15764  trirec0  15775  apdiff  15779  redc0  15788  reap0  15789  cndcap  15790  neap0mkv  15800