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	$$⊢\exists x\left(x=y\wedge \phi \right)\to \left(x=y\to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		exnalimn	$$⊢\exists x\left(x=y\wedge \phi \right)\leftrightarrow \neg \forall x\left(x=y\to \neg \phi \right)$$
2		ax12v2	$$⊢x=y\to \left(\neg \phi \to \forall x\left(x=y\to \neg \phi \right)\right)$$
3	2	con1d	$$⊢x=y\to \left(\neg \forall x\left(x=y\to \neg \phi \right)\to \phi \right)$$
4	1 3	biimtrid	$$⊢x=y\to \left(\exists x\left(x=y\wedge \phi \right)\to \phi \right)$$
5	4	com12	$$⊢\exists x\left(x=y\wedge \phi \right)\to \left(x=y\to \phi \right)$$