Metamath Proof Explorer


Theorem rexlimdvva

Description: Inference from Theorem 19.23 of Margaris p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014)

Ref Expression
Hypothesis rexlimdvva.1 φ x A y B ψ χ
Assertion rexlimdvva φ x A y B ψ χ

Proof

Step Hyp Ref Expression
1 rexlimdvva.1 φ x A y B ψ χ
2 1 ex φ x A y B ψ χ
3 2 rexlimdvv φ x A y B ψ χ