Theorem ralrimivva 2632

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

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

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is referenced by:  swopo  4446  sosng  4843  fcof1  5979  fliftfund  5993  isoresbr  6005  isocnv  6007  f1oiso  6022  oveqrspc2v  6102  caovclg  6232  caovcomg  6235  off  6305  caofrss  6324  caofdig  6326  oprssdmm  6395  dmmpog  6435  fnmpoovd  6441  fmpoco  6442  poxp  6458  f1od2  6461  suppofss1dcl  6494  suppofss2dcl  6495  eroprf  6892  dom2lem  7048  xpf1o  7134  fidifsnid  7163  nnwetri  7213  undiffi  7222  fidcenumlemim  7259  supmoti  7323  supsnti  7335  supisoti  7340  difinfsnlem  7429  nninfwlpor  7504  netap  7610  2omotaplemap  7613  cc2lem  7622  addlocpr  7893  mullocpr  7928  cauappcvgprlemloc  8009  cauappcvgprlemlim  8018  caucvgprlemloc  8032  caucvgprprlemloc  8060  suplocexprlemloc  8078  suplocsrlemb  8163  rereceu  8246  axpre-suploclemres  8258  ltordlem  8800  cju  9281  exbtwnz  10663  frec2uzf1od  10821  frec2uzisod  10822  frecuzrdgrrn  10823  frec2uzrdg  10824  frecuzrdgrcl  10825  frecuzrdgsuc  10829  frecuzrdgrclt  10830  frecuzrdgg  10831  frecuzrdgsuctlem  10838  seqvalcd  10876  seqovcd  10882  seq3caopr3  10906  seq3caopr2  10908  seqcaopr2g  10909  iseqf1olemqf1o  10921  seq3homo  10942  seqhomog  10945  seqfeq4g  10946  seq3distr  10947  fimaxq  11248  zfz1isolem1  11270  wrd2ind  11473  rsqrmo  11771  climcn2  12053  addcn2  12054  mulcn2  12056  fsum2dlemstep  12179  fisumcom2  12183  cvgratnn  12276  fprodcl2lem  12350  fprod2dlemstep  12367  fprodcom2fi  12371  divalglemeunn  12666  divalglemeuneg  12668  bezoutlemeu  12762  isprm6  12903  pw2dvdseu  12924  crth  12980  eulerthlemh  12987  4sqlemffi  13153  ennnfonelemim  13293  nninfdclemf1  13321  unbendc  13323  imasaddfnlemg  13612  ercpbl  13629  plusffng  13662  mgmplusf  13663  opifismgmdc  13668  issgrpd  13704  sgrppropd  13705  ismndd  13727  mndpropd  13730  issubmnd  13732  mndinvmod  13735  mhmpropd  13750  idmhm  13753  mhmf1o  13754  issubmd  13758  mndissubm  13759  submid  13761  0mhm  13770  resmhm  13771  resmhm2  13772  resmhm2b  13773  mhmco  13774  grppropd  13799  grpsubf  13861  dfgrp3m  13881  mhmmnd  13896  mhmfmhm  13897  mulgfng  13904  issubg4m  13973  grpissubg  13974  isnsg3  13987  0nsg  13994  nsgid  13995  isghmd  14032  ghmmhm  14033  idghm  14039  ghmnsgima  14048  ghmnsgpreima  14049  ghmf1  14053  kerf1ghm  14054  ghmf1o  14055  cmnsubm  14089  ghmcmn  14108  invghm  14110  ablnsg  14115  imasabl  14117  srgfcl  14251  srglmhm  14271  srgrmhm  14272  isrhm2d  14445  subrngringnsg  14486  issubrng2  14491  subrngintm  14493  issubrg2  14522  subrgintm  14524  aprap  14571  aprlring  14573  islmodd  14602  lmodscaf  14619  lmodprop2d  14657  islssmd  14668  islss4  14691  lsspropdg  14740  issubrgd  14761  dflidl2rng  14790  rnglidlmmgm  14805  expghmap  14914  mulgghm2  14915  znf1o  14958  znidom  14964  tgclb  15089  txbas  15282  txcnp  15295  txcnmpt  15297  cnmpt21  15315  txswaphmeo  15345  isxmetd  15371  isxmet2d  15372  xmettpos  15394  blfvalps  15409  xmetresbl  15464  metss2  15522  comet  15523  bdmet  15526  bdmopn  15528  xmetxp  15531  qtopbasss  15545  elcncf1di  15603  cncfcdm  15606  mulc1cncf  15613  cncfco  15615  dedekindeulemloc  15643  dedekindeu  15647  dedekindicclemloc  15652  dedekindicclemicc  15656  ivthinclemloc  15665  dich0  15676  dvmptfsum  15749  mpodvdsmulf1o  16018  fsumdvdsmul  16019  gausslemma2dlem1f1o  16093  lgseisenlem2  16104  lgsquadlemsfi  16108  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  usgredgreu  16371  uspgredg2vtxeu  16373  uspgredg2v  16376  usgredg2v  16379  vtxedgfi  16444  vtxlpfi  16445  dichmul0or  16674  sssneq  16946  exmidsbthrlem  16972  cvgcmp2n  16987  trirec0  16998  apdiff  17002  redc0  17012  reap0  17013  cndcap  17014  neap0mkv  17024