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

Metamath Proof Explorer

Theorem icheq

Description: In an equality of setvar variables, the setvar variables are interchangeable. (Contributed by AV, 29-Jul-2023)

Ref Expression
Assertion icheq [ 𝑥 ⇄ 𝑦 ] 𝑥 = 𝑦

Proof

Step Hyp Ref Expression
1 equsb3r ⊢ ( [ 𝑧 / 𝑦 ] 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 )
2 1 2sbbii ⊢ ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝑥 = 𝑦 ↔ [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝑥 = 𝑧 )
3 equsb3 ⊢ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 )
4 3 sbbii ⊢ ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝑥 = 𝑧 ↔ [ 𝑥 / 𝑧 ] 𝑦 = 𝑧 )
5 equsb3r ⊢ ( [ 𝑥 / 𝑧 ] 𝑦 = 𝑧 ↔ 𝑦 = 𝑥 )
6 equcom ⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
7 5 6 bitri ⊢ ( [ 𝑥 / 𝑧 ] 𝑦 = 𝑧 ↔ 𝑥 = 𝑦 )
8 2 4 7 3bitri ⊢ ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 )
9 8 gen2 ⊢ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 )
10 df-ich ⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝑥 = 𝑦 ↔ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 ) )
11 9 10 mpbir ⊢ [ 𝑥 ⇄ 𝑦 ] 𝑥 = 𝑦