Metamath Proof Explorer

Theorem nfnid

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

Ref Expression
Assertion nfnid ⊢ ¬ Ⅎ _ x x

Proof

Step Hyp Ref Expression
1 dtru ⊢ ¬ ∀ z z = w
2 ax-ext ⊢ ∀ y y ∈ z ↔ y ∈ w → z = w
3 2 sps ⊢ ∀ w ∀ y y ∈ z ↔ y ∈ w → z = w
4 3 alimi ⊢ ∀ z ∀ w ∀ y y ∈ z ↔ y ∈ w → ∀ z z = w
5 1 4 mto ⊢ ¬ ∀ z ∀ w ∀ y y ∈ z ↔ y ∈ w
6 df-nfc ⊢ Ⅎ _ x x ↔ ∀ y Ⅎ x y ∈ x
7 sbnf2 ⊢ Ⅎ x y ∈ x ↔ ∀ z ∀ w z x y ∈ x ↔ w x y ∈ x
8 elsb4 ⊢ z x y ∈ x ↔ y ∈ z
9 elsb4 ⊢ w x y ∈ x ↔ y ∈ w
10 8 9 bibi12i ⊢ z x y ∈ x ↔ w x y ∈ x ↔ y ∈ z ↔ y ∈ w
11 10 2albii ⊢ ∀ z ∀ w z x y ∈ x ↔ w x y ∈ x ↔ ∀ z ∀ w y ∈ z ↔ y ∈ w
12 7 11 bitri ⊢ Ⅎ x y ∈ x ↔ ∀ z ∀ w y ∈ z ↔ y ∈ w
13 12 albii ⊢ ∀ y Ⅎ x y ∈ x ↔ ∀ y ∀ z ∀ w y ∈ z ↔ y ∈ w
14 alrot3 ⊢ ∀ y ∀ z ∀ w y ∈ z ↔ y ∈ w ↔ ∀ z ∀ w ∀ y y ∈ z ↔ y ∈ w
15 6 13 14 3bitri ⊢ Ⅎ _ x x ↔ ∀ z ∀ w ∀ y y ∈ z ↔ y ∈ w
16 5 15 mtbir ⊢ ¬ Ⅎ _ x x