Theorem ichcom

Description: The interchangeability of setvar variables is commutative. (Contributed by AV, 20-Aug-2023)

	Ref	Expression
Assertion	ichcom	⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜓 ↔ [ 𝑦 ⇄ 𝑥 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		alcom	⊢ ( ∀ 𝑏 ∀ 𝑎 ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ) )
2		sbcom2	⊢ ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜓 ↔ [ 𝑎 / 𝑦 ] [ 𝑏 / 𝑥 ] 𝜓 )
3		sbcom2	⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 )
4	2 3	bibi12i	⊢ ( ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ( [ 𝑎 / 𝑦 ] [ 𝑏 / 𝑥 ] 𝜓 ↔ [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 ) )
5	4	2albii	⊢ ( ∀ 𝑎 ∀ 𝑏 ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑦 ] [ 𝑏 / 𝑥 ] 𝜓 ↔ [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 ) )
6	1 5	bitri	⊢ ( ∀ 𝑏 ∀ 𝑎 ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑦 ] [ 𝑏 / 𝑥 ] 𝜓 ↔ [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 ) )
7		dfich2	⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜓 ↔ ∀ 𝑏 ∀ 𝑎 ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ) )
8		dfich2	⊢ ( [ 𝑦 ⇄ 𝑥 ] 𝜓 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑦 ] [ 𝑏 / 𝑥 ] 𝜓 ↔ [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 ) )
9	6 7 8	3bitr4i	⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜓 ↔ [ 𝑦 ⇄ 𝑥 ] 𝜓 )