Theorem dfich2

Description: Alternate definition of the propery of a wff ph that the setvar variables x and y are interchangeable. (Contributed by AV and WL, 6-Aug-2023)

	Ref	Expression
Assertion	dfich2	$$⊢\left[x\rightleftarrows y\right]\phi \leftrightarrow \forall a\forall b\left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/x\right]\left[a/y\right]\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ich	$$⊢\left[x\rightleftarrows y\right]\phi \leftrightarrow \forall x\forall y\left(\left[x/z\right]\left[y/x\right]\left[z/y\right]\phi \leftrightarrow \phi \right)$$
2		nfs1v	$$⊢Ⅎy\left[b/y\right]\phi$$
3	2	nfsbv	$$⊢Ⅎy\left[a/x\right]\left[b/y\right]\phi$$
4	3	nfsbv	$$⊢Ⅎy\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi$$
5		nfv	$$⊢Ⅎa\phi$$
6	4 5	sbbib	$$⊢\forall y\left(\left[y/a\right]\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \phi \right)\leftrightarrow \forall a\left(\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[a/y\right]\phi \right)$$
7	6	albii	$$⊢\forall x\forall y\left(\left[y/a\right]\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \phi \right)\leftrightarrow \forall x\forall a\left(\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[a/y\right]\phi \right)$$
8		sbco4	$$⊢\left[y/a\right]\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[x/z\right]\left[y/x\right]\left[z/y\right]\phi$$
9	8	bibi1i	$$⊢\left(\left[y/a\right]\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \phi \right)\leftrightarrow \left(\left[x/z\right]\left[y/x\right]\left[z/y\right]\phi \leftrightarrow \phi \right)$$
10	9	2albii	$$⊢\forall x\forall y\left(\left[y/a\right]\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \phi \right)\leftrightarrow \forall x\forall y\left(\left[x/z\right]\left[y/x\right]\left[z/y\right]\phi \leftrightarrow \phi \right)$$
11		alcom	$$⊢\forall x\forall a\left(\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[a/y\right]\phi \right)\leftrightarrow \forall a\forall x\left(\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[a/y\right]\phi \right)$$
12		nfs1v	$$⊢Ⅎx\left[a/x\right]\left[b/y\right]\phi$$
13		nfv	$$⊢Ⅎb\left[a/y\right]\phi$$
14	12 13	sbbib	$$⊢\forall x\left(\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[a/y\right]\phi \right)\leftrightarrow \forall b\left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/x\right]\left[a/y\right]\phi \right)$$
15	14	albii	$$⊢\forall a\forall x\left(\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[a/y\right]\phi \right)\leftrightarrow \forall a\forall b\left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/x\right]\left[a/y\right]\phi \right)$$
16	11 15	bitri	$$⊢\forall x\forall a\left(\left[x/b\right]\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[a/y\right]\phi \right)\leftrightarrow \forall a\forall b\left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/x\right]\left[a/y\right]\phi \right)$$
17	7 10 16	3bitr3i	$$⊢\forall x\forall y\left(\left[x/z\right]\left[y/x\right]\left[z/y\right]\phi \leftrightarrow \phi \right)\leftrightarrow \forall a\forall b\left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/x\right]\left[a/y\right]\phi \right)$$
18	1 17	bitri	$$⊢\left[x\rightleftarrows y\right]\phi \leftrightarrow \forall a\forall b\left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/x\right]\left[a/y\right]\phi \right)$$