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

Metamath Proof Explorer

Theorem ichal

Description: Move a universal quantifier inside interchangeability. (Contributed by SN, 30-Aug-2023)

Ref Expression
Assertion ichal ⊢ ∀ x a ⇄ b φ → a ⇄ b ∀ x φ

Proof

Step Hyp Ref Expression
1 ax-11 ⊢ ∀ x ∀ a ∀ b a u b a u b φ ↔ φ → ∀ a ∀ x ∀ b a u b a u b φ ↔ φ
2 ax-11 ⊢ ∀ x ∀ b a u b a u b φ ↔ φ → ∀ b ∀ x a u b a u b φ ↔ φ
3 2 alimi ⊢ ∀ a ∀ x ∀ b a u b a u b φ ↔ φ → ∀ a ∀ b ∀ x a u b a u b φ ↔ φ
4 sbal ⊢ u b ∀ x φ ↔ ∀ x u b φ
5 4 2sbbii ⊢ a u b a u b ∀ x φ ↔ a u b a ∀ x u b φ
6 sbal ⊢ b a ∀ x u b φ ↔ ∀ x b a u b φ
7 6 sbbii ⊢ a u b a ∀ x u b φ ↔ a u ∀ x b a u b φ
8 sbal ⊢ a u ∀ x b a u b φ ↔ ∀ x a u b a u b φ
9 5 7 8 3bitri ⊢ a u b a u b ∀ x φ ↔ ∀ x a u b a u b φ
10 albi ⊢ ∀ x a u b a u b φ ↔ φ → ∀ x a u b a u b φ ↔ ∀ x φ
11 9 10 bitrid ⊢ ∀ x a u b a u b φ ↔ φ → a u b a u b ∀ x φ ↔ ∀ x φ
12 11 2alimi ⊢ ∀ a ∀ b ∀ x a u b a u b φ ↔ φ → ∀ a ∀ b a u b a u b ∀ x φ ↔ ∀ x φ
13 1 3 12 3syl ⊢ ∀ x ∀ a ∀ b a u b a u b φ ↔ φ → ∀ a ∀ b a u b a u b ∀ x φ ↔ ∀ x φ
14 df-ich ⊢ a ⇄ b φ ↔ ∀ a ∀ b a u b a u b φ ↔ φ
15 14 albii ⊢ ∀ x a ⇄ b φ ↔ ∀ x ∀ a ∀ b a u b a u b φ ↔ φ
16 df-ich ⊢ a ⇄ b ∀ x φ ↔ ∀ a ∀ b a u b a u b ∀ x φ ↔ ∀ x φ
17 13 15 16 3imtr4i ⊢ ∀ x a ⇄ b φ → a ⇄ b ∀ x φ