Theorem ralrimivv 2625

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  ralrimivva  2626  ralrimdvv  2628  reuind  3024  ssrel2  4842  f1o2ndf1  6426  smoiso  6535  nndifsnid  6742  receuap  8945  lbreu  9221  0subm  13714  insubm  13715  iscmnd  14032  quscrng  14698  tgcl  14946  topbas  14949  epttop  14972  restbasg  15050  txbas  15140  txbasval  15149  blfps  15291  blf  15292  blbas  15315