Theorem nfeqf

Description: A variable is effectively not free in an equality if it is not either of the involved variables. F/ version of ax-c9 . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 6-Oct-2016) Remove dependency on ax-11 . (Revised by Wolf Lammen, 6-Sep-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	nfeqf	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to Ⅎzx=y$$

Proof

Step	Hyp	Ref	Expression
1		nfna1	$$⊢Ⅎz\neg \forall zz=x$$
2		nfna1	$$⊢Ⅎz\neg \forall zz=y$$
3	1 2	nfan	$$⊢Ⅎz\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)$$
4		equvinva	$$⊢x=y\to \exists w\left(x=w\wedge y=w\right)$$
5		dveeq1	$$⊢\neg \forall zz=x\to \left(x=w\to \forall zx=w\right)$$
6	5	imp	$$⊢\left(\neg \forall zz=x\wedge x=w\right)\to \forall zx=w$$
7		dveeq1	$$⊢\neg \forall zz=y\to \left(y=w\to \forall zy=w\right)$$
8	7	imp	$$⊢\left(\neg \forall zz=y\wedge y=w\right)\to \forall zy=w$$
9		equtr2	$$⊢\left(x=w\wedge y=w\right)\to x=y$$
10	9	alanimi	$$⊢\left(\forall zx=w\wedge \forall zy=w\right)\to \forall zx=y$$
11	6 8 10	syl2an	$$⊢\left(\left(\neg \forall zz=x\wedge x=w\right)\wedge \left(\neg \forall zz=y\wedge y=w\right)\right)\to \forall zx=y$$
12	11	an4s	$$⊢\left(\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\wedge \left(x=w\wedge y=w\right)\right)\to \forall zx=y$$
13	12	ex	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(\left(x=w\wedge y=w\right)\to \forall zx=y\right)$$
14	13	exlimdv	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(\exists w\left(x=w\wedge y=w\right)\to \forall zx=y\right)$$
15	4 14	syl5	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(x=y\to \forall zx=y\right)$$
16	3 15	nf5d	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to Ⅎzx=y$$