Theorem ax12fromc15

Description: Rederivation of Axiom ax-12 from ax-c15 , ax-c11 (used through dral1-o ), and other older axioms. See Theorem axc15 for the derivation of ax-c15 from ax-12 .

An open problem is whether we can prove this using ax-c11n instead of ax-c11 .

This proof uses newer axioms ax-4 and ax-6 , but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 and ax-c10 . (Contributed by NM, 22-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ax12fromc15	$$⊢x=y\to \left(\forall y\phi \to \forall x\left(x=y\to \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		biidd	$$⊢\forall xx=y\to \left(\phi \leftrightarrow \phi \right)$$
2	1	dral1-o	$$⊢\forall xx=y\to \left(\forall x\phi \leftrightarrow \forall y\phi \right)$$
3		ax-1	$$⊢\phi \to \left(x=y\to \phi \right)$$
4	3	alimi	$$⊢\forall x\phi \to \forall x\left(x=y\to \phi \right)$$
5	2 4	syl6bir	$$⊢\forall xx=y\to \left(\forall y\phi \to \forall x\left(x=y\to \phi \right)\right)$$
6	5	a1d	$$⊢\forall xx=y\to \left(x=y\to \left(\forall y\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
7		ax-c5	$$⊢\forall y\phi \to \phi$$
8		ax-c15	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
9	7 8	syl7	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\forall y\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
10	6 9	pm2.61i	$$⊢x=y\to \left(\forall y\phi \to \forall x\left(x=y\to \phi \right)\right)$$