Theorem ralrimivva 2626

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  swopo  4429  sosng  4825  fcof1  5958  fliftfund  5972  isoresbr  5984  isocnv  5986  f1oiso  6001  oveqrspc2v  6079  caovclg  6209  caovcomg  6212  off  6281  caofrss  6300  caofdig  6302  oprssdmm  6367  dmmpog  6407  fnmpoovd  6413  fmpoco  6414  poxp  6430  f1od2  6433  suppofss1dcl  6466  suppofss2dcl  6467  eroprf  6864  dom2lem  7013  xpf1o  7099  fidifsnid  7128  nnwetri  7178  undiffi  7187  fidcenumlemim  7224  supmoti  7286  supsnti  7298  supisoti  7303  difinfsnlem  7392  nninfwlpor  7467  netap  7570  2omotaplemap  7573  cc2lem  7582  addlocpr  7853  mullocpr  7888  cauappcvgprlemloc  7969  cauappcvgprlemlim  7978  caucvgprlemloc  7992  caucvgprprlemloc  8020  suplocexprlemloc  8038  suplocsrlemb  8123  rereceu  8206  axpre-suploclemres  8218  ltordlem  8758  cju  9237  exbtwnz  10614  frec2uzf1od  10772  frec2uzisod  10773  frecuzrdgrrn  10774  frec2uzrdg  10775  frecuzrdgrcl  10776  frecuzrdgsuc  10780  frecuzrdgrclt  10781  frecuzrdgg  10782  frecuzrdgsuctlem  10789  seqvalcd  10827  seqovcd  10833  seq3caopr3  10857  seq3caopr2  10859  seqcaopr2g  10860  iseqf1olemqf1o  10872  seq3homo  10893  seqhomog  10896  seqfeq4g  10897  seq3distr  10898  fimaxq  11198  zfz1isolem1  11216  wrd2ind  11419  rsqrmo  11716  climcn2  11998  addcn2  11999  mulcn2  12001  fsum2dlemstep  12124  fisumcom2  12128  cvgratnn  12221  fprodcl2lem  12295  fprod2dlemstep  12312  fprodcom2fi  12316  divalglemeunn  12611  divalglemeuneg  12613  bezoutlemeu  12707  isprm6  12848  pw2dvdseu  12869  crth  12925  eulerthlemh  12932  4sqlemffi  13098  ennnfonelemim  13192  nninfdclemf1  13220  unbendc  13222  imasaddfnlemg  13544  ercpbl  13561  plusffng  13595  mgmplusf  13596  opifismgmdc  13601  issgrpd  13642  sgrppropd  13643  ismndd  13667  mndpropd  13670  issubmnd  13672  mndinvmod  13675  mhmpropd  13696  idmhm  13699  mhmf1o  13700  issubmd  13704  mndissubm  13705  submid  13707  0mhm  13716  resmhm  13717  resmhm2  13718  resmhm2b  13719  mhmco  13720  grppropd  13747  grpsubf  13809  dfgrp3m  13829  mhmmnd  13850  mhmfmhm  13851  mulgfng  13858  issubg4m  13927  grpissubg  13928  isnsg3  13941  0nsg  13948  nsgid  13949  isghmd  13986  ghmmhm  13987  idghm  13993  ghmnsgima  14002  ghmnsgpreima  14003  ghmf1  14007  kerf1ghm  14008  ghmf1o  14009  ghmcmn  14061  invghm  14063  ablnsg  14068  imasabl  14070  srgfcl  14134  srglmhm  14154  srgrmhm  14155  isrhm2d  14327  subrngringnsg  14367  issubrng2  14372  subrngintm  14374  issubrg2  14403  subrgintm  14405  aprap  14449  aprlring  14451  islmodd  14458  lmodscaf  14475  lmodprop2d  14513  islssmd  14524  islss4  14547  lsspropdg  14596  issubrgd  14617  dflidl2rng  14646  rnglidlmmgm  14661  expghmap  14772  mulgghm2  14773  znf1o  14816  znidom  14822  tgclb  14947  txbas  15140  txcnp  15153  txcnmpt  15155  cnmpt21  15173  txswaphmeo  15203  isxmetd  15229  isxmet2d  15230  xmettpos  15252  blfvalps  15267  xmetresbl  15322  metss2  15380  comet  15381  bdmet  15384  bdmopn  15386  xmetxp  15389  qtopbasss  15403  elcncf1di  15461  cncfcdm  15464  mulc1cncf  15471  cncfco  15473  dedekindeulemloc  15501  dedekindeu  15505  dedekindicclemloc  15510  dedekindicclemicc  15514  ivthinclemloc  15523  dich0  15534  dvmptfsum  15607  mpodvdsmulf1o  15875  fsumdvdsmul  15876  gausslemma2dlem1f1o  15950  lgseisenlem2  15961  lgsquadlemsfi  15965  lgsquadlem1  15967  lgsquadlem2  15968  lgsquadlem3  15969  usgredgreu  16228  uspgredg2vtxeu  16230  uspgredg2v  16233  usgredg2v  16236  vtxedgfi  16301  vtxlpfi  16302  sssneq  16793  exmidsbthrlem  16819  cvgcmp2n  16834  trirec0  16845  apdiff  16849  redc0  16859  reap0  16860  cndcap  16861  trimul0or  16862  neap0mkv  16872