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	|- ( [ x <> y ] ph <-> A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		vy	|- y
2		wph	|- ph
3	2 0 1	wich	|- [ x <> y ] ph
4		va	|- a
5	2 1 4	wsb	|- [ a / y ] ph
6	5 0 1	wsb	|- [ y / x ] [ a / y ] ph
7	6 4 0	wsb	|- [ x / a ] [ y / x ] [ a / y ] ph
8	7 2	wb	|- ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph )
9	8 1	wal	|- A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph )
10	9 0	wal	|- A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph )
11	3 10	wb	|- ( [ x <> y ] ph <-> A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph ) )