This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ¬ Ⅎ 𝑥 𝑥

Proof

Step Hyp Ref Expression
1 dtruALT2 ⊢ ¬ ∀ 𝑧 𝑧 = 𝑤
2 ax-ext ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) → 𝑧 = 𝑤 )
3 2 sps ⊢ ( ∀ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) → 𝑧 = 𝑤 )
4 3 alimi ⊢ ( ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) → ∀ 𝑧 𝑧 = 𝑤 )
5 1 4 mto ⊢ ¬ ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 )
6 df-nfc ⊢ ( Ⅎ 𝑥 𝑥 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝑥 )
7 sbnf2 ⊢ ( Ⅎ 𝑥 𝑦 ∈ 𝑥 ↔ ∀ 𝑧 ∀ 𝑤 ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ [ 𝑤 / 𝑥 ] 𝑦 ∈ 𝑥 ) )
8 elsb2 ⊢ ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧 )
9 elsb2 ⊢ ( [ 𝑤 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑤 )
10 8 9 bibi12i ⊢ ( ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ [ 𝑤 / 𝑥 ] 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
11 10 2albii ⊢ ( ∀ 𝑧 ∀ 𝑤 ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ [ 𝑤 / 𝑥 ] 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑤 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
12 7 11 bitri ⊢ ( Ⅎ 𝑥 𝑦 ∈ 𝑥 ↔ ∀ 𝑧 ∀ 𝑤 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
13 12 albii ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
14 alrot3 ⊢ ( ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
15 6 13 14 3bitri ⊢ ( Ⅎ 𝑥 𝑥 ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑤 ) )
16 5 15 mtbir ⊢ ¬ Ⅎ 𝑥 𝑥