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	$$⊢x=y$$
Assertion	dtrucor	$$⊢x\ne y$$

Proof

Step	Hyp	Ref	Expression
1		dtrucor.1	$$⊢x=y$$
2		dtru	$$⊢\neg \forall xx=y$$
3	2	pm2.21i	$$⊢\forall xx=y\to x\ne y$$
4	3 1	mpg	$$⊢x\ne y$$