Theorem nfnid 5375

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 dtruALT2 5370 in its proof. (Contributed by Mario Carneiro, 8-Oct-2016.)

Assertion

Ref	Expression
nfnid	⊢ ¬ Ⅎ𝑥𝑥

Proof of Theorem nfnid

Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dtruALT2 5370	. . 3 ⊢ ¬ ∀𝑧 𝑧 = 𝑤
2		ax-ext 2708	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → 𝑧 = 𝑤)
3	2	sps 2185	. . . 4 ⊢ (∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → 𝑧 = 𝑤)
4	3	alimi 1811	. . 3 ⊢ (∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → ∀𝑧 𝑧 = 𝑤)
5	1, 4	mto 197	. 2 ⊢ ¬ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤)
6		df-nfc 2892	. . 3 ⊢ (Ⅎ𝑥𝑥 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝑥)
7		sbnf2 2361	. . . . 5 ⊢ (Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑧∀𝑤([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥))
8		elsb2 2125	. . . . . . 7 ⊢ ([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)
9		elsb2 2125	. . . . . . 7 ⊢ ([𝑤 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑤)
10	8, 9	bibi12i 339	. . . . . 6 ⊢ (([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
11	10	2albii 1820	. . . . 5 ⊢ (∀𝑧∀𝑤([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥) ↔ ∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
12	7, 11	bitri 275	. . . 4 ⊢ (Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
13	12	albii 1819	. . 3 ⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑦∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
14		alrot3 2160	. . 3 ⊢ (∀𝑦∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) ↔ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
15	6, 13, 14	3bitri 297	. 2 ⊢ (Ⅎ𝑥𝑥 ↔ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
16	5, 15	mtbir 323	1 ⊢ ¬ Ⅎ𝑥𝑥

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538  Ⅎwnf 1783  [wsb 2064  Ⅎwnfc 2890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-nul 5306  ax-pow 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-sb 2065  df-nfc 2892

This theorem is referenced by:  nfcvb  5376