Metamath Proof Explorer


Theorem rexsn

Description: Convert an existential quantification restricted to a singleton to a substitution. (Contributed by Jeff Madsen, 5-Jan-2011)

Ref Expression
Hypotheses ralsn.1 A V
ralsn.2 x = A φ ψ
Assertion rexsn x A φ ψ

Proof

Step Hyp Ref Expression
1 ralsn.1 A V
2 ralsn.2 x = A φ ψ
3 2 rexsng A V x A φ ψ
4 1 3 ax-mp x A φ ψ