Theorem ralrimivv 2513

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)

Hypothesis

Ref	Expression
ralrimivv.1	|- ( ph -> ( ( x e. A /\ y e. B ) -> ps ) )

Assertion

Ref	Expression
ralrimivv	|- ( ph -> A. x e. A A. y e. B ps )

Distinct variable groups:   x, y, ph   y, A

Allowed substitution hints:   ps( x, y)   A( x)   B( x, y)

Proof of Theorem ralrimivv

Step	Hyp	Ref	Expression
1		ralrimivv.1	. . . 4 |- ( ph -> ( ( x e. A /\ y e. B ) -> ps ) )
2	1	expd 256	. . 3 |- ( ph -> ( x e. A -> ( y e. B -> ps ) ) )
3	2	ralrimdv 2511	. 2 |- ( ph -> ( x e. A -> A. y e. B ps ) )
4	3	ralrimiv 2504	1 |- ( ph -> A. x e. A A. y e. B ps )

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

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421

This theorem is referenced by:  ralrimivva  2514  ralrimdvv  2516  reuind  2889  ssrel2  4629  f1o2ndf1  6125  smoiso  6199  nndifsnid  6403  receuap  8430  lbreu  8703  tgcl  12233  topbas  12236  epttop  12259  restbasg  12337  txbas  12427  txbasval  12436  blfps  12578  blf  12579  blbas  12602