Theorem nfnid 5383

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 5378 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 5378	. . 3 ⊢ ¬ ∀𝑧 𝑧 = 𝑤
2		ax-ext 2700	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → 𝑧 = 𝑤)
3	2	sps 2177	. . . 4 ⊢ (∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → 𝑧 = 𝑤)
4	3	alimi 1806	. . 3 ⊢ (∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → ∀𝑧 𝑧 = 𝑤)
5	1, 4	mto 196	. 2 ⊢ ¬ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤)
6		df-nfc 2881	. . 3 ⊢ (Ⅎ𝑥𝑥 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝑥)
7		sbnf2 2352	. . . . 5 ⊢ (Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑧∀𝑤([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥))
8		elsb2 2117	. . . . . . 7 ⊢ ([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)
9		elsb2 2117	. . . . . . 7 ⊢ ([𝑤 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑤)
10	8, 9	bibi12i 338	. . . . . 6 ⊢ (([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
11	10	2albii 1815	. . . . 5 ⊢ (∀𝑧∀𝑤([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥) ↔ ∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
12	7, 11	bitri 274	. . . 4 ⊢ (Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
13	12	albii 1814	. . 3 ⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑦∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
14		alrot3 2153	. . 3 ⊢ (∀𝑦∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) ↔ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
15	6, 13, 14	3bitri 296	. 2 ⊢ (Ⅎ𝑥𝑥 ↔ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
16	5, 15	mtbir 322	1 ⊢ ¬ Ⅎ𝑥𝑥

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1532  Ⅎwnf 1778  [wsb 2061  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-nul 5314  ax-pow 5373

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1775  df-nf 1779  df-sb 2062  df-nfc 2881

This theorem is referenced by:  nfcvb  5384