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

Ref Expression
Assertion nfnid ⊢¬Ⅎ_xx

Proof

Step Hyp Ref Expression
1 dtruALT2 ⊢¬∀zz=w
2 ax-ext ⊢∀yy∈z↔y∈w→z=w
3 2 sps ⊢∀w∀yy∈z↔y∈w→z=w
4 3 alimi ⊢∀z∀w∀yy∈z↔y∈w→∀zz=w
5 1 4 mto ⊢¬∀z∀w∀yy∈z↔y∈w
6 df-nfc ⊢Ⅎ_xx↔∀yℲxy∈x
7 sbnf2 ⊢Ⅎxy∈x↔∀z∀wzxy∈x↔wxy∈x
8 elsb2 ⊢zxy∈x↔y∈z
9 elsb2 ⊢wxy∈x↔y∈w
10 8 9 bibi12i ⊢zxy∈x↔wxy∈x↔y∈z↔y∈w
11 10 2albii ⊢∀z∀wzxy∈x↔wxy∈x↔∀z∀wy∈z↔y∈w
12 7 11 bitri ⊢Ⅎxy∈x↔∀z∀wy∈z↔y∈w
13 12 albii ⊢∀yℲxy∈x↔∀y∀z∀wy∈z↔y∈w
14 alrot3 ⊢∀y∀z∀wy∈z↔y∈w↔∀z∀w∀yy∈z↔y∈w
15 6 13 14 3bitri ⊢Ⅎ_xx↔∀z∀w∀yy∈z↔y∈w
16 5 15 mtbir ⊢¬Ⅎ_xx