Theorem nfnid 5298

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 5293 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 5293	. . 3 ⊢ ¬ ∀𝑧 𝑧 = 𝑤
2		ax-ext 2709	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → 𝑧 = 𝑤)
3	2	sps 2178	. . . 4 ⊢ (∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → 𝑧 = 𝑤)
4	3	alimi 1814	. . 3 ⊢ (∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → ∀𝑧 𝑧 = 𝑤)
5	1, 4	mto 196	. 2 ⊢ ¬ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤)
6		df-nfc 2889	. . 3 ⊢ (Ⅎ𝑥𝑥 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝑥)
7		sbnf2 2356	. . . . 5 ⊢ (Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑧∀𝑤([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥))
8		elsb2 2123	. . . . . . 7 ⊢ ([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)
9		elsb2 2123	. . . . . . 7 ⊢ ([𝑤 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑤)
10	8, 9	bibi12i 340	. . . . . 6 ⊢ (([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
11	10	2albii 1823	. . . . 5 ⊢ (∀𝑧∀𝑤([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥) ↔ ∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
12	7, 11	bitri 274	. . . 4 ⊢ (Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
13	12	albii 1822	. . 3 ⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑦∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
14		alrot3 2157	. . 3 ⊢ (∀𝑦∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) ↔ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
15	6, 13, 14	3bitri 297	. 2 ⊢ (Ⅎ𝑥𝑥 ↔ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
16	5, 15	mtbir 323	1 ⊢ ¬ Ⅎ𝑥𝑥

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537  Ⅎwnf 1786  [wsb 2067  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5230  ax-pow 5288

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787  df-sb 2068  df-nfc 2889

This theorem is referenced by:  nfcvb  5299