Theorem absnw

Description: Replace ax-10 , ax-11 , ax-12 in absn with a substitution hypothesis. (Contributed by SN, 27-May-2025)

	Ref	Expression
Hypothesis	absnw.y	|- ( x = y -> ( ph <-> ps ) )
Assertion	absnw	|- ( { x | ph } = { Y } <-> A. x ( ph <-> x = Y ) )

Proof

Step	Hyp	Ref	Expression
1		absnw.y	|- ( x = y -> ( ph <-> ps ) )
2		df-sn	|- { Y } = { x | x = Y }
3	2	eqeq2i	|- ( { x | ph } = { Y } <-> { x | ph } = { x | x = Y } )
4		eqeq1	|- ( x = y -> ( x = Y <-> y = Y ) )
5	1 4	abbibw	|- ( { x | ph } = { x | x = Y } <-> A. x ( ph <-> x = Y ) )
6	3 5	bitri	|- ( { x | ph } = { Y } <-> A. x ( ph <-> x = Y ) )