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	syl5bb	⊢ ( ∀ 𝑥 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) → ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜑 ) )
12	11	2alimi	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑥 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) → ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜑 ) )
13	1 3 12	3syl	⊢ ( ∀ 𝑥 ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) → ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜑 ) )
14		df-ich	⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) )
15	14	albii	⊢ ( ∀ 𝑥 [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) )
16		df-ich	⊢ ( [ 𝑎 ⇄ 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜑 ) )
17	13 15 16	3imtr4i	⊢ ( ∀ 𝑥 [ 𝑎 ⇄ 𝑏 ] 𝜑 → [ 𝑎 ⇄ 𝑏 ] ∀ 𝑥 𝜑 )