Theorem ralrimivv 2631

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 258	. . 3 |- ( ph -> ( x e. A -> ( y e. B -> ps ) ) )
3	2	ralrimdv 2629	. 2 |- ( ph -> ( x e. A -> A. y e. B ps ) )
4	3	ralrimiv 2622	1 |- ( ph -> A. x e. A A. y e. B ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   A.wral 2528

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralrimivva  2632  ralrimdvv  2634  reuind  3031  ssrel2  4867  f1o2ndf1  6468  smoiso  6578  nndifsnid  6785  receuap  9007  lbreu  9283  0subm  13849  insubm  13850  iscmnd  14190  quscrng  14978  tgcl  15307  topbas  15310  epttop  15333  restbasg  15411  txbas  15501  txbasval  15510  blfps  15652  blf  15653  blbas  15676