Theorem rexlimdvv 2496

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)

Hypothesis

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

Assertion

Ref	Expression
rexlimdvv	|- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

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

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

Proof of Theorem rexlimdvv

Step	Hyp	Ref	Expression
1		rexlimdvv.1	. . . 4 |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
2	1	expdimp 256	. . 3 |- ( ( ph /\ x e. A ) -> ( y e. B -> ( ps -> ch ) ) )
3	2	rexlimdv 2489	. 2 |- ( ( ph /\ x e. A ) -> ( E. y e. B ps -> ch ) )
4	3	rexlimdva 2490	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1439   E.wrex 2361

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-i5r 1474

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-ral 2365  df-rex 2366

This theorem is referenced by:  rexlimdvva  2497  f1oiso2  5620  xpdom2  6601  genpcdl  7132  genpcuu  7133  distrlem1prl  7195  distrlem1pru  7196  distrlem5prl  7199  distrlem5pru  7200  recexprlemss1l  7248  recexprlemss1u  7249  qaddcl  9174  qmulcl  9176  isummo  10827  dvdsgcd  11333  gcddiv  11340