Theorem ralrimivv 2547

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 2545	. 2 |- ( ph -> ( x e. A -> A. y e. B ps ) )
4	3	ralrimiv 2538	1 |- ( ph -> A. x e. A A. y e. B ps )

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

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449

This theorem is referenced by:  ralrimivva  2548  ralrimdvv  2550  reuind  2931  ssrel2  4694  f1o2ndf1  6196  smoiso  6270  nndifsnid  6475  receuap  8566  lbreu  8840  tgcl  12704  topbas  12707  epttop  12730  restbasg  12808  txbas  12898  txbasval  12907  blfps  13049  blf  13050  blbas  13073