ax12

Description: Rederivation of Axiom ax-12 from ax12v (used only via sp ), axc11r , and axc15 (on top of Tarski's FOL). Since this version depends on ax-13 , usage of the weaker ax12v , ax12w , ax12i are preferred. (Contributed by NM, 22-Jan-2007) Proof uses contemporary axioms. (Revised by Wolf Lammen, 8-Aug-2020) (Proof shortened by BJ, 4-Jul-2021) (New usage is discouraged.)

		Ref	Expression
	Assertion	ax12	$⊢ x = y \to (\forall y φ \to \forall x (x = y \to φ))$

Proof

Step	Hyp	Ref	Expression
1		axc11r	$⊢ \forall x x = y \to (\forall y φ \to \forall x φ)$
2		ala1	$⊢ \forall x φ \to \forall x (x = y \to φ)$
3	1 2	syl6	$⊢ \forall x x = y \to (\forall y φ \to \forall x (x = y \to φ))$
4	3	a1d	$⊢ \forall x x = y \to (x = y \to (\forall y φ \to \forall x (x = y \to φ)))$
5		sp	$⊢ \forall y φ \to φ$
6		axc15	$⊢ \neg \forall x x = y \to (x = y \to (φ \to \forall x (x = y \to φ)))$
7	5 6	syl7	$⊢ \neg \forall x x = y \to (x = y \to (\forall y φ \to \forall x (x = y \to φ)))$
8	4 7	pm2.61i	$⊢ x = y \to (\forall y φ \to \forall x (x = y \to φ))$

Metamath Proof Explorer

Theorem ax12

Proof