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		dtru	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦
3	2	pm2.21i	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 ≠ 𝑦 )
4	3 1	mpg	⊢ 𝑥 ≠ 𝑦