This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (x = y \land φ) \to (x = y \to φ)$

Proof

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