Theorem ralrimivv 2558

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  ralrimivva  2559  ralrimdvv  2561  reuind  2944  ssrel2  4718  f1o2ndf1  6232  smoiso  6306  nndifsnid  6511  receuap  8629  lbreu  8905  0subm  12877  insubm  12878  iscmnd  13107  tgcl  13704  topbas  13707  epttop  13730  restbasg  13808  txbas  13898  txbasval  13907  blfps  14049  blf  14050  blbas  14073