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 ( ∀ 𝑥 [ 𝑎 ⇄ 𝑏 ] 𝜑 → [ 𝑎 ⇄ 𝑏 ] ∀ 𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 ax-11 ⊢ ( ∀ 𝑥 ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) → ∀ 𝑎 ∀ 𝑥 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) )
2 ax-11 ⊢ ( ∀ 𝑥 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) → ∀ 𝑏 ∀ 𝑥 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) )
3 2 alimi ⊢ ( ∀ 𝑎 ∀ 𝑥 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) → ∀ 𝑎 ∀ 𝑏 ∀ 𝑥 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) )
4 sbal ⊢ ( [ 𝑢 / 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑢 / 𝑏 ] 𝜑 )
5 4 2sbbii ⊢ ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ∀ 𝑥 𝜑 ↔ [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] ∀ 𝑥 [ 𝑢 / 𝑏 ] 𝜑 )
6 sbal ⊢ ( [ 𝑏 / 𝑎 ] ∀ 𝑥 [ 𝑢 / 𝑏 ] 𝜑 ↔ ∀ 𝑥 [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
7 6 sbbii ⊢ ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] ∀ 𝑥 [ 𝑢 / 𝑏 ] 𝜑 ↔ [ 𝑎 / 𝑢 ] ∀ 𝑥 [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
8 sbal ⊢ ( [ 𝑎 / 𝑢 ] ∀ 𝑥 [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ ∀ 𝑥 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
9 5 7 8 3bitri ⊢ ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
10 albi ⊢ ( ∀ 𝑥 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) → ( ∀ 𝑥 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ ∀ 𝑥 𝜑 ) )
11 9 10 bitrid ⊢ ( ∀ 𝑥 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) → ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜑 ) )
12 11 2alimi ⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑥 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) → ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜑 ) )
13 1 3 12 3syl ⊢ ( ∀ 𝑥 ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) → ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜑 ) )
14 df-ich ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) )
15 14 albii ⊢ ( ∀ 𝑥 [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) )
16 df-ich ⊢ ( [ 𝑎 ⇄ 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜑 ) )
17 13 15 16 3imtr4i ⊢ ( ∀ 𝑥 [ 𝑎 ⇄ 𝑏 ] 𝜑 → [ 𝑎 ⇄ 𝑏 ] ∀ 𝑥 𝜑 )