Theorem ralrimivva 2517

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 114	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ps ) )
3	2	ralrimivv 2516	1 |- ( ph -> A. x e. A A. y e. B ps )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1481   A.wral 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422

This theorem is referenced by:  swopo  4236  sosng  4620  fcof1  5692  fliftfund  5706  isoresbr  5718  isocnv  5720  f1oiso  5735  caovclg  5931  caovcomg  5934  off  6002  caofrss  6014  oprssdmm  6077  dmmpog  6115  fnmpoovd  6120  fmpoco  6121  poxp  6137  f1od2  6140  eroprf  6530  dom2lem  6674  xpf1o  6746  fidifsnid  6773  nnwetri  6812  undiffi  6821  fidcenumlemim  6848  supmoti  6888  supsnti  6900  supisoti  6905  difinfsnlem  6992  cc2lem  7098  addlocpr  7368  mullocpr  7403  cauappcvgprlemloc  7484  cauappcvgprlemlim  7493  caucvgprlemloc  7507  caucvgprprlemloc  7535  suplocexprlemloc  7553  suplocsrlemb  7638  rereceu  7721  axpre-suploclemres  7733  ltordlem  8268  cju  8743  exbtwnz  10059  frec2uzf1od  10210  frec2uzisod  10211  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  frecuzrdgsuctlem  10227  seqvalcd  10263  seqovcd  10267  seq3caopr3  10285  seq3caopr2  10286  iseqf1olemqf1o  10297  seq3homo  10314  seq3distr  10317  fimaxq  10605  zfz1isolem1  10615  rsqrmo  10831  climcn2  11110  addcn2  11111  mulcn2  11113  fsum2dlemstep  11235  fisumcom2  11239  cvgratnn  11332  divalglemeunn  11654  divalglemeuneg  11656  bezoutlemeu  11731  isprm6  11861  pw2dvdseu  11882  crth  11936  ennnfonelemim  11973  tgclb  12273  txbas  12466  txcnp  12479  txcnmpt  12481  cnmpt21  12499  txswaphmeo  12529  isxmetd  12555  isxmet2d  12556  xmettpos  12578  blfvalps  12593  xmetresbl  12648  metss2  12706  comet  12707  bdmet  12710  bdmopn  12712  xmetxp  12715  qtopbasss  12729  elcncf1di  12774  cncffvrn  12777  mulc1cncf  12784  cncfco  12786  dedekindeulemloc  12805  dedekindeu  12809  dedekindicclemloc  12814  dedekindicclemicc  12818  ivthinclemloc  12827  sssneq  13370  exmidsbthrlem  13392  cvgcmp2n  13403  trirec0  13412  apdiff  13416