Theorem nfnid 5293

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 5288 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		dtru 5288	. . 3 ⊢ ¬ ∀𝑧 𝑧 = 𝑤
2		ax-ext 2709	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → 𝑧 = 𝑤)
3	2	sps 2180	. . . 4 ⊢ (∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → 𝑧 = 𝑤)
4	3	alimi 1815	. . 3 ⊢ (∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) → ∀𝑧 𝑧 = 𝑤)
5	1, 4	mto 196	. 2 ⊢ ¬ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤)
6		df-nfc 2888	. . 3 ⊢ (Ⅎ𝑥𝑥 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝑥)
7		sbnf2 2356	. . . . 5 ⊢ (Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑧∀𝑤([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥))
8		elsb2 2125	. . . . . . 7 ⊢ ([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)
9		elsb2 2125	. . . . . . 7 ⊢ ([𝑤 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑤)
10	8, 9	bibi12i 339	. . . . . 6 ⊢ (([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
11	10	2albii 1824	. . . . 5 ⊢ (∀𝑧∀𝑤([𝑧 / 𝑥]𝑦 ∈ 𝑥 ↔ [𝑤 / 𝑥]𝑦 ∈ 𝑥) ↔ ∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
12	7, 11	bitri 274	. . . 4 ⊢ (Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
13	12	albii 1823	. . 3 ⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝑥 ↔ ∀𝑦∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
14		alrot3 2159	. . 3 ⊢ (∀𝑦∀𝑧∀𝑤(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤) ↔ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
15	6, 13, 14	3bitri 296	. 2 ⊢ (Ⅎ𝑥𝑥 ↔ ∀𝑧∀𝑤∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤))
16	5, 15	mtbir 322	1 ⊢ ¬ Ⅎ𝑥𝑥

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537  Ⅎwnf 1787  [wsb 2068  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225  ax-pow 5283

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788  df-sb 2069  df-nfc 2888

This theorem is referenced by:  nfcvb  5294