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  7089  undiffi  7098  fidcenumlemim  7130  supmoti  7171  supsnti  7183  supisoti  7188  difinfsnlem  7277  nninfwlpor  7352  netap  7451  2omotaplemap  7454  cc2lem  7463  addlocpr  7734  mullocpr  7769  cauappcvgprlemloc  7850  cauappcvgprlemlim  7859  caucvgprlemloc  7873  caucvgprprlemloc  7901  suplocexprlemloc  7919  suplocsrlemb  8004  rereceu  8087  axpre-suploclemres  8099  ltordlem  8640  cju  9119  exbtwnz  10482  frec2uzf1od  10640  frec2uzisod  10641  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  frecuzrdgsuctlem  10657  seqvalcd  10695  seqovcd  10701  seq3caopr3  10725  seq3caopr2  10727  seqcaopr2g  10728  iseqf1olemqf1o  10740  seq3homo  10761  seqhomog  10764  seqfeq4g  10765  seq3distr  10766  fimaxq  11062  zfz1isolem1  11075  wrd2ind  11271  rsqrmo  11554  climcn2  11836  addcn2  11837  mulcn2  11839  fsum2dlemstep  11961  fisumcom2  11965  cvgratnn  12058  fprodcl2lem  12132  fprod2dlemstep  12149  fprodcom2fi  12153  divalglemeunn  12448  divalglemeuneg  12450  bezoutlemeu  12544  isprm6  12685  pw2dvdseu  12706  crth  12762  eulerthlemh  12769  4sqlemffi  12935  ennnfonelemim  13011  nninfdclemf1  13039  unbendc  13041  imasaddfnlemg  13363  ercpbl  13380  plusffng  13414  mgmplusf  13415  opifismgmdc  13420  issgrpd  13461  sgrppropd  13462  ismndd  13486  mndpropd  13489  issubmnd  13491  mndinvmod  13494  mhmpropd  13515  idmhm  13518  mhmf1o  13519  issubmd  13523  mndissubm  13524  submid  13526  0mhm  13535  resmhm  13536  resmhm2  13537  resmhm2b  13538  mhmco  13539  grppropd  13566  grpsubf  13628  dfgrp3m  13648  mhmmnd  13669  mhmfmhm  13670  mulgfng  13677  issubg4m  13746  grpissubg  13747  isnsg3  13760  0nsg  13767  nsgid  13768  isghmd  13805  ghmmhm  13806  idghm  13812  ghmnsgima  13821  ghmnsgpreima  13822  ghmf1  13826  kerf1ghm  13827  ghmf1o  13828  ghmcmn  13880  invghm  13882  ablnsg  13887  imasabl  13889  srgfcl  13952  srglmhm  13972  srgrmhm  13973  isrhm2d  14145  subrngringnsg  14185  issubrng2  14190  subrngintm  14192  issubrg2  14221  subrgintm  14223  aprap  14266  islmodd  14273  lmodscaf  14290  lmodprop2d  14328  islssmd  14339  islss4  14362  lsspropdg  14411  issubrgd  14432  dflidl2rng  14461  rnglidlmmgm  14476  expghmap  14587  mulgghm2  14588  znf1o  14631  znidom  14637  tgclb  14755  txbas  14948  txcnp  14961  txcnmpt  14963  cnmpt21  14981  txswaphmeo  15011  isxmetd  15037  isxmet2d  15038  xmettpos  15060  blfvalps  15075  xmetresbl  15130  metss2  15188  comet  15189  bdmet  15192  bdmopn  15194  xmetxp  15197  qtopbasss  15211  elcncf1di  15269  cncfcdm  15272  mulc1cncf  15279  cncfco  15281  dedekindeulemloc  15309  dedekindeu  15313  dedekindicclemloc  15318  dedekindicclemicc  15322  ivthinclemloc  15331  dich0  15342  dvmptfsum  15415  mpodvdsmulf1o  15680  fsumdvdsmul  15681  gausslemma2dlem1f1o  15755  lgseisenlem2  15766  lgsquadlemsfi  15770  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  usgredgreu  16030  uspgredg2vtxeu  16032  uspgredg2v  16035  usgredg2v  16038  vtxedgfi  16049  vtxlpfi  16050  sssneq  16455  exmidsbthrlem  16478  cvgcmp2n  16489  trirec0  16500  apdiff  16504  redc0  16513  reap0  16514  cndcap  16515  neap0mkv  16525