Metamath Proof Explorer

Theorem ichal

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

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

Proof

Step Hyp Ref Expression
1 ax-11 ⊢∀x∀a∀baubaubφ↔φ→∀a∀x∀baubaubφ↔φ
2 ax-11 ⊢∀x∀baubaubφ↔φ→∀b∀xaubaubφ↔φ
3 2 alimi ⊢∀a∀x∀baubaubφ↔φ→∀a∀b∀xaubaubφ↔φ
4 sbal ⊢ub∀xφ↔∀xubφ
5 4 2sbbii ⊢aubaub∀xφ↔auba∀xubφ
6 sbal ⊢ba∀xubφ↔∀xbaubφ
7 6 sbbii ⊢auba∀xubφ↔au∀xbaubφ
8 sbal ⊢au∀xbaubφ↔∀xaubaubφ
9 5 7 8 3bitri ⊢aubaub∀xφ↔∀xaubaubφ
10 albi ⊢∀xaubaubφ↔φ→∀xaubaubφ↔∀xφ
11 9 10 bitrid ⊢∀xaubaubφ↔φ→aubaub∀xφ↔∀xφ
12 11 2alimi ⊢∀a∀b∀xaubaubφ↔φ→∀a∀baubaub∀xφ↔∀xφ
13 1 3 12 3syl ⊢∀x∀a∀baubaubφ↔φ→∀a∀baubaub∀xφ↔∀xφ
14 df-ich ⊢a⇄bφ↔∀a∀baubaubφ↔φ
15 14 albii ⊢∀xa⇄bφ↔∀x∀a∀baubaubφ↔φ
16 df-ich ⊢a⇄b∀xφ↔∀a∀baubaub∀xφ↔∀xφ
17 13 15 16 3imtr4i ⊢∀xa⇄bφ→a⇄b∀xφ