Definition df-ich

Description: Define the property of a wff ph that the setvar variables x and y are interchangeable. For an alternate definition using implicit substitution and a temporary setvar variable see ichcircshi . Another, equivalent definition using two temporary setvar variables is provided in dfich2 . (Contributed by AV, 29-Jul-2023)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		vy	$$setvary$$
2		wph	$$wff\phi$$
3	2 0 1	wich	$$wff\left[x\rightleftarrows y\right]\phi$$
4		va	$$setvara$$
5	2 1 4	wsb	$$wff\left[a/y\right]\phi$$
6	5 0 1	wsb	$$wff\left[y/x\right]\left[a/y\right]\phi$$
7	6 4 0	wsb	$$wff\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi$$
8	7 2	wb	$$wff\left(\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \phi \right)$$
9	8 1	wal	$$wff\forall y\left(\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \phi \right)$$
10	9 0	wal	$$wff\forall x\forall y\left(\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \phi \right)$$
11	3 10	wb	$$wff\left(\left[x\rightleftarrows y\right]\phi \leftrightarrow \forall x\forall y\left(\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \phi \right)\right)$$