Theorem ichal

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

	Ref	Expression
Assertion	ichal	$$⊢\forall x\left[a\rightleftarrows b\right]\phi \to \left[a\rightleftarrows b\right]\forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		ax-11	$$⊢\forall x\forall a\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)\to \forall a\forall x\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)$$
2		ax-11	$$⊢\forall x\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)\to \forall b\forall x\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)$$
3	2	alimi	$$⊢\forall a\forall x\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)\to \forall a\forall b\forall x\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)$$
4		sbal	$$⊢\left[u/b\right]\forall x\phi \leftrightarrow \forall x\left[u/b\right]\phi$$
5	4	2sbbii	$$⊢\left[a/u\right]\left[b/a\right]\left[u/b\right]\forall x\phi \leftrightarrow \left[a/u\right]\left[b/a\right]\forall x\left[u/b\right]\phi$$
6		sbal	$$⊢\left[b/a\right]\forall x\left[u/b\right]\phi \leftrightarrow \forall x\left[b/a\right]\left[u/b\right]\phi$$
7	6	sbbii	$$⊢\left[a/u\right]\left[b/a\right]\forall x\left[u/b\right]\phi \leftrightarrow \left[a/u\right]\forall x\left[b/a\right]\left[u/b\right]\phi$$
8		sbal	$$⊢\left[a/u\right]\forall x\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \forall x\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi$$
9	5 7 8	3bitri	$$⊢\left[a/u\right]\left[b/a\right]\left[u/b\right]\forall x\phi \leftrightarrow \forall x\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi$$
10		albi	$$⊢\forall x\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)\to \left(\forall x\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \forall x\phi \right)$$
11	9 10	bitrid	$$⊢\forall x\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)\to \left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\forall x\phi \leftrightarrow \forall x\phi \right)$$
12	11	2alimi	$$⊢\forall a\forall b\forall x\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)\to \forall a\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\forall x\phi \leftrightarrow \forall x\phi \right)$$
13	1 3 12	3syl	$$⊢\forall x\forall a\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)\to \forall a\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\forall x\phi \leftrightarrow \forall x\phi \right)$$
14		df-ich	$$⊢\left[a\rightleftarrows b\right]\phi \leftrightarrow \forall a\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)$$
15	14	albii	$$⊢\forall x\left[a\rightleftarrows b\right]\phi \leftrightarrow \forall x\forall a\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)$$
16		df-ich	$$⊢\left[a\rightleftarrows b\right]\forall x\phi \leftrightarrow \forall a\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\forall x\phi \leftrightarrow \forall x\phi \right)$$
17	13 15 16	3imtr4i	$$⊢\forall x\left[a\rightleftarrows b\right]\phi \to \left[a\rightleftarrows b\right]\forall x\phi$$