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

Metamath Proof Explorer

Theorem dtrucor

Description: Corollary of dtru . This example illustrates the danger of blindly trusting the standard Deduction Theorem without accounting for free variables: the theorem form of this deduction is not valid, as shown by dtrucor2 . (Contributed by NM, 27-Jun-2002)

		Ref	Expression
	Hypothesis	dtrucor.1	⊢ 𝑥 = 𝑦
	Assertion	dtrucor	⊢ 𝑥 ≠ 𝑦

Proof

Step	Hyp	Ref	Expression
1		dtrucor.1	⊢ 𝑥 = 𝑦
2		dtruALT2	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦
3	2	pm2.21i	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 ≠ 𝑦 )
4	3 1	mpg	⊢ 𝑥 ≠ 𝑦