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

Metamath Proof Explorer

Theorem pm13.14

Description: Theorem *13.14 in WhiteheadRussell p. 178. (Contributed by Andrew Salmon, 3-Jun-2011)

		Ref	Expression
	Assertion	pm13.14	$⊢ (\underset{˙}{[} A / x \underset{˙}{]} φ \land \neg φ) \to x \neq A$

Step	Hyp	Ref	Expression
1		sbceq1a	$⊢ x = A \to (φ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} φ)$
2	1	biimprcd	$⊢ \underset{˙}{[} A / x \underset{˙}{]} φ \to (x = A \to φ)$
3	2	necon3bd	$⊢ \underset{˙}{[} A / x \underset{˙}{]} φ \to (\neg φ \to x \neq A)$
4	3	imp	$⊢ (\underset{˙}{[} A / x \underset{˙}{]} φ \land \neg φ) \to x \neq A$