Metamath Proof Explorer


Theorem rexlim2d

Description: Inference removing two restricted quantifiers. Same as rexlimdvv , but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses rexlim2d.x
|- F/ x ph
rexlim2d.y
|- F/ y ph
rexlim2d.3
|- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
Assertion rexlim2d
|- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

Proof

Step Hyp Ref Expression
1 rexlim2d.x
 |-  F/ x ph
2 rexlim2d.y
 |-  F/ y ph
3 rexlim2d.3
 |-  ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
4 nfv
 |-  F/ x ch
5 nfv
 |-  F/ y x e. A
6 2 5 nfan
 |-  F/ y ( ph /\ x e. A )
7 nfv
 |-  F/ y ch
8 3 expdimp
 |-  ( ( ph /\ x e. A ) -> ( y e. B -> ( ps -> ch ) ) )
9 6 7 8 rexlimd
 |-  ( ( ph /\ x e. A ) -> ( E. y e. B ps -> ch ) )
10 9 ex
 |-  ( ph -> ( x e. A -> ( E. y e. B ps -> ch ) ) )
11 1 4 10 rexlimd
 |-  ( ph -> ( E. x e. A E. y e. B ps -> ch ) )