Theorem euabsn2w

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

	Ref	Expression
Hypotheses	absnw.y	|- ( x = y -> ( ph <-> ps ) )
	euabsn2w.z	|- ( x = z -> ( ph <-> th ) )
Assertion	euabsn2w	|- ( E! x ph <-> E. y { x | ph } = { y } )

Proof

Step	Hyp	Ref	Expression
1		absnw.y	|- ( x = y -> ( ph <-> ps ) )
2		euabsn2w.z	|- ( x = z -> ( ph <-> th ) )
3	2 1	eu6w	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
4	2	absnw	|- ( { x | ph } = { y } <-> A. x ( ph <-> x = y ) )
5	4	exbii	|- ( E. y { x | ph } = { y } <-> E. y A. x ( ph <-> x = y ) )
6	3 5	bitr4i	|- ( E! x ph <-> E. y { x | ph } = { y } )