Theorem equvel

Description: A variable elimination law for equality with no distinct variable requirements. Compare equvini . Usage of this theorem is discouraged because it depends on ax-13 . Use equvelv when possible. (Contributed by NM, 1-Mar-2013) (Proof shortened by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 15-Jun-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	equvel	$$⊢\forall z\left(z=x\leftrightarrow z=y\right)\to x=y$$

Proof

Step	Hyp	Ref	Expression
1		albi	$$⊢\forall z\left(z=x\leftrightarrow z=y\right)\to \left(\forall zz=x\leftrightarrow \forall zz=y\right)$$
2		ax6e	$$⊢\exists zz=y$$
3		biimpr	$$⊢\left(z=x\leftrightarrow z=y\right)\to \left(z=y\to z=x\right)$$
4		ax7	$$⊢z=x\to \left(z=y\to x=y\right)$$
5	3 4	syli	$$⊢\left(z=x\leftrightarrow z=y\right)\to \left(z=y\to x=y\right)$$
6	5	com12	$$⊢z=y\to \left(\left(z=x\leftrightarrow z=y\right)\to x=y\right)$$
7	2 6	eximii	$$⊢\exists z\left(\left(z=x\leftrightarrow z=y\right)\to x=y\right)$$
8	7	19.35i	$$⊢\forall z\left(z=x\leftrightarrow z=y\right)\to \exists zx=y$$
9	4	spsd	$$⊢z=x\to \left(\forall zz=y\to x=y\right)$$
10	9	sps	$$⊢\forall zz=x\to \left(\forall zz=y\to x=y\right)$$
11	10	a1dd	$$⊢\forall zz=x\to \left(\forall zz=y\to \left(\exists zx=y\to x=y\right)\right)$$
12		nfeqf	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to Ⅎzx=y$$
13	12	19.9d	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(\exists zx=y\to x=y\right)$$
14	13	ex	$$⊢\neg \forall zz=x\to \left(\neg \forall zz=y\to \left(\exists zx=y\to x=y\right)\right)$$
15	11 14	bija	$$⊢\left(\forall zz=x\leftrightarrow \forall zz=y\right)\to \left(\exists zx=y\to x=y\right)$$
16	1 8 15	sylc	$$⊢\forall z\left(z=x\leftrightarrow z=y\right)\to x=y$$