Metamath Proof Explorer


Theorem rexsns

Description: Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015) (Revised by NM, 22-Aug-2018)

Ref Expression
Assertion rexsns x A φ [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 velsn x A x = A
2 1 anbi1i x A φ x = A φ
3 2 exbii x x A φ x x = A φ
4 df-rex x A φ x x A φ
5 sbc5 [˙A / x]˙ φ x x = A φ
6 3 4 5 3bitr4i x A φ [˙A / x]˙ φ