Theorem absnsb

Description: If the class abstraction { x | ph } associated with the wff ph is a singleton, the wff is true for the singleton element. (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	absnsb	|- ( { x | ph } = { y } -> [ y / x ] ph )

Proof

Step	Hyp	Ref	Expression
1		abid	|- ( x e. { x | ph } <-> ph )
2		velsn	|- ( x e. { y } <-> x = y )
3	1 2	bibi12i	|- ( ( x e. { x | ph } <-> x e. { y } ) <-> ( ph <-> x = y ) )
4		biimpr	|- ( ( ph <-> x = y ) -> ( x = y -> ph ) )
5	3 4	sylbi	|- ( ( x e. { x | ph } <-> x e. { y } ) -> ( x = y -> ph ) )
6	5	alimi	|- ( A. x ( x e. { x | ph } <-> x e. { y } ) -> A. x ( x = y -> ph ) )
7		nfab1	|- F/_ x { x | ph }
8		nfcv	|- F/_ x { y }
9	7 8	cleqf	|- ( { x | ph } = { y } <-> A. x ( x e. { x | ph } <-> x e. { y } ) )
10		sb6	|- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
11	6 9 10	3imtr4i	|- ( { x | ph } = { y } -> [ y / x ] ph )