Theorem ax12ev2

Description: Version of ax12v2 rewritten to use an existential quantifier. One direction of sbalex without the universal quantifier, avoiding ax-10 . (Contributed by SN, 14-Aug-2025)

	Ref	Expression
Assertion	ax12ev2	|- ( E. x ( x = y /\ ph ) -> ( x = y -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		exnalimn	|- ( E. x ( x = y /\ ph ) <-> -. A. x ( x = y -> -. ph ) )
2		ax12v2	|- ( x = y -> ( -. ph -> A. x ( x = y -> -. ph ) ) )
3	2	con1d	|- ( x = y -> ( -. A. x ( x = y -> -. ph ) -> ph ) )
4	1 3	biimtrid	|- ( x = y -> ( E. x ( x = y /\ ph ) -> ph ) )
5	4	com12	|- ( E. x ( x = y /\ ph ) -> ( x = y -> ph ) )