Metamath Proof Explorer

Theorem ichcom

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

Ref Expression
Assertion ichcom ⊢ x ⇄ y ψ ↔ y ⇄ x ψ

Proof

Step Hyp Ref Expression
1 alcom ⊢ ∀ b ∀ a b x a y ψ ↔ a x b y ψ ↔ ∀ a ∀ b b x a y ψ ↔ a x b y ψ
2 sbcom2 ⊢ b x a y ψ ↔ a y b x ψ
3 sbcom2 ⊢ a x b y ψ ↔ b y a x ψ
4 2 3 bibi12i ⊢ b x a y ψ ↔ a x b y ψ ↔ a y b x ψ ↔ b y a x ψ
5 4 2albii ⊢ ∀ a ∀ b b x a y ψ ↔ a x b y ψ ↔ ∀ a ∀ b a y b x ψ ↔ b y a x ψ
6 1 5 bitri ⊢ ∀ b ∀ a b x a y ψ ↔ a x b y ψ ↔ ∀ a ∀ b a y b x ψ ↔ b y a x ψ
7 dfich2 ⊢ x ⇄ y ψ ↔ ∀ b ∀ a b x a y ψ ↔ a x b y ψ
8 dfich2 ⊢ y ⇄ x ψ ↔ ∀ a ∀ b a y b x ψ ↔ b y a x ψ
9 6 7 8 3bitr4i ⊢ x ⇄ y ψ ↔ y ⇄ x ψ