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	⊢ ¬ Ⅎ 𝑥 𝑥

Proof

Step	Hyp	Ref	Expression
1		dtru	⊢ ¬ ∀ 𝑧 𝑧 = 𝑤
2		ax-ext	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) → 𝑧 = 𝑤 )
3	2	sps	⊢ ( ∀ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) → 𝑧 = 𝑤 )
4	3	alimi	⊢ ( ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) → ∀ 𝑧 𝑧 = 𝑤 )
5	1 4	mto	⊢ ¬ ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 )
6		df-nfc	⊢ ( Ⅎ 𝑥 𝑥 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝑥 )
7		sbnf2	⊢ ( Ⅎ 𝑥 𝑦 ∈ 𝑥 ↔ ∀ 𝑧 ∀ 𝑤 ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ [ 𝑤 / 𝑥 ] 𝑦 ∈ 𝑥 ) )
8		elsb4	⊢ ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧 )
9		elsb4	⊢ ( [ 𝑤 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑤 )
10	8 9	bibi12i	⊢ ( ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ [ 𝑤 / 𝑥 ] 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
11	10	2albii	⊢ ( ∀ 𝑧 ∀ 𝑤 ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ [ 𝑤 / 𝑥 ] 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑤 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
12	7 11	bitri	⊢ ( Ⅎ 𝑥 𝑦 ∈ 𝑥 ↔ ∀ 𝑧 ∀ 𝑤 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
13	12	albii	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
14		alrot3	⊢ ( ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
15	6 13 14	3bitri	⊢ ( Ⅎ 𝑥 𝑥 ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
16	5 15	mtbir	⊢ ¬ Ⅎ 𝑥 𝑥