Theorem nfnid 5340

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 5335 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 5335	. . 3 ⊢ ¬ ∀𝑧 𝑧 = 𝑤
2		ax-ext 2735	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → 𝑧 = 𝑤)
3	2	sps 2224	. . . 4 ⊢ (∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → 𝑧 = 𝑤)
4	3	alimi 1843	. . 3 ⊢ (∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → ∀𝑧 𝑧 = 𝑤)
5	1, 4	mto 200	. 2 ⊢ ¬ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤)
6		df-nfc 2912	. . 3 ⊢ (Ⅎ𝑥𝑥 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝑥)
7		sbnf2 2390	. . . . 5 ⊢ (Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑧∀𝑤([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥))
8		elsb2 2163	. . . . . . 7 ⊢ ([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)
9		elsb2 2163	. . . . . . 7 ⊢ ([𝑤 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑤)
10	8, 9	bibi12i 342	. . . . . 6 ⊢ (([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
11	10	2albii 1852	. . . . 5 ⊢ (∀𝑧∀𝑤([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥) ↔ ∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
12	7, 11	bitri 278	. . . 4 ⊢ (Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
13	12	albii 1851	. . 3 ⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑦∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
14		alrot3 2199	. . 3 ⊢ (∀𝑦∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) ↔ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
15	6, 13, 14	3bitri 300	. 2 ⊢ (Ⅎ𝑥𝑥 ↔ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
16	5, 15	mtbir 326	1 ⊢ ¬ Ⅎ𝑥𝑥

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1567  Ⅎwnf 1815  [wsb 2100  Ⅎwnfc 2910

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-nul 5262  ax-pow 5330

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-sb 2101  df-nfc 2912

This theorem is used by:  nfcvb  5341