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

Metamath Proof Explorer

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 ⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜓 ↔ [ 𝑦 ⇄ 𝑥 ] 𝜓 )