Theorem nfnid

Description: A setvar variable is not free from itself. This theorem is not true in a one-element domain, as illustrated by the use of dtru in its proof. (Contributed by Mario Carneiro, 8-Oct-2016)

	Ref	Expression
Assertion	nfnid	|- -. F/_ x x

Proof

Step	Hyp	Ref	Expression
1		dtru	|- -. A. z z = w
2		ax-ext	|- ( A. y ( y e. z <-> y e. w ) -> z = w )
3	2	sps	|- ( A. w A. y ( y e. z <-> y e. w ) -> z = w )
4	3	alimi	|- ( A. z A. w A. y ( y e. z <-> y e. w ) -> A. z z = w )
5	1 4	mto	|- -. A. z A. w A. y ( y e. z <-> y e. w )
6		df-nfc	|- ( F/_ x x <-> A. y F/ x y e. x )
7		sbnf2	|- ( F/ x y e. x <-> A. z A. w ( [ z / x ] y e. x <-> [ w / x ] y e. x ) )
8		elsb2	|- ( [ z / x ] y e. x <-> y e. z )
9		elsb2	|- ( [ w / x ] y e. x <-> y e. w )
10	8 9	bibi12i	|- ( ( [ z / x ] y e. x <-> [ w / x ] y e. x ) <-> ( y e. z <-> y e. w ) )
11	10	2albii	|- ( A. z A. w ( [ z / x ] y e. x <-> [ w / x ] y e. x ) <-> A. z A. w ( y e. z <-> y e. w ) )
12	7 11	bitri	|- ( F/ x y e. x <-> A. z A. w ( y e. z <-> y e. w ) )
13	12	albii	|- ( A. y F/ x y e. x <-> A. y A. z A. w ( y e. z <-> y e. w ) )
14		alrot3	|- ( A. y A. z A. w ( y e. z <-> y e. w ) <-> A. z A. w A. y ( y e. z <-> y e. w ) )
15	6 13 14	3bitri	|- ( F/_ x x <-> A. z A. w A. y ( y e. z <-> y e. w ) )
16	5 15	mtbir	|- -. F/_ x x