Definition df-ich 46104

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

Assertion

Ref	Expression
df-ich	⊢ ([𝑥⇄𝑦]𝜑 ↔ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑))

Distinct variable groups:   𝜑,𝑎   𝑥,𝑎   𝑦,𝑎

Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Definition df-ich

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4	1, 2, 3	wich 46103	. 2 wff [𝑥⇄𝑦]𝜑
5		va	. . . . . . . 8 setvar 𝑎
6	1, 3, 5	wsb 2067	. . . . . . 7 wff [𝑎 / 𝑦]𝜑
7	6, 2, 3	wsb 2067	. . . . . 6 wff [𝑦 / 𝑥][𝑎 / 𝑦]𝜑
8	7, 5, 2	wsb 2067	. . . . 5 wff [𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑
9	8, 1	wb 205	. . . 4 wff ([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)
10	9, 3	wal 1539	. . 3 wff ∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)
11	10, 2	wal 1539	. 2 wff ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)
12	4, 11	wb 205	1 wff ([𝑥⇄𝑦]𝜑 ↔ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑))

This definition is referenced by:  nfich1  46105  nfich2  46106  ichv  46107  ichf  46108  ichid  46109  icht  46110  ichbidv  46111  ichcircshi  46112  ichan  46113  ichn  46114  dfich2  46116  icheq  46120  ichal  46124  ich2exprop  46129