Theorem ralsngf

Description: Restricted universal quantification over a singleton. (Contributed by NM, 14-Dec-2005) (Revised by AV, 3-Apr-2023)

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

Proof

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