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	⊢ [ 𝑥 ⇄ 𝑦 ] 𝑥 = 𝑦