Theorem rexsngf

Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012) (Revised by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	rexsngf.1	|- F/ x ps
	rexsngf.2	|- ( x = A -> ( ph <-> ps ) )
Assertion	rexsngf	|- ( A e. V -> ( E. x e. { A } ph <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		rexsngf.1	|- F/ x ps
2		rexsngf.2	|- ( x = A -> ( ph <-> ps ) )
3		rexsns	|- ( E. x e. { A } ph <-> [. A / x ]. ph )
4	1 2	sbciegf	|- ( A e. V -> ( [. A / x ]. ph <-> ps ) )
5	3 4	bitrid	|- ( A e. V -> ( E. x e. { A } ph <-> ps ) )