Definition df-ich 47433

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 47441. Another, equivalent definition using two temporary setvar variables is provided in dfich2 47445. (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 47432	. 2 wff [𝑥⇄𝑦]𝜑
5		va	. . . . . . . 8 setvar 𝑎
6	1, 3, 5	wsb 2064	. . . . . . 7 wff [𝑎 / 𝑦]𝜑
7	6, 2, 3	wsb 2064	. . . . . 6 wff [𝑦 / 𝑥][𝑎 / 𝑦]𝜑
8	7, 5, 2	wsb 2064	. . . . 5 wff [𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑
9	8, 1	wb 206	. . . 4 wff ([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)
10	9, 3	wal 1538	. . 3 wff ∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)
11	10, 2	wal 1538	. 2 wff ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)
12	4, 11	wb 206	1 wff ([𝑥⇄𝑦]𝜑 ↔ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑))

This definition is referenced by:  nfich1  47434  nfich2  47435  ichv  47436  ichf  47437  ichid  47438  icht  47439  ichbidv  47440  ichcircshi  47441  ichan  47442  ichn  47443  dfich2  47445  icheq  47449  ichal  47453  ich2exprop  47458