Definition df-ich 47447

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 47455. Another, equivalent definition using two temporary setvar variables is provided in dfich2 47459. (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 47446	. 2 wff [𝑥⇄𝑦]𝜑
5		va	. . . . . . . 8 setvar 𝑎
6	1, 3, 5	wsb 2065	. . . . . . 7 wff [𝑎 / 𝑦]𝜑
7	6, 2, 3	wsb 2065	. . . . . 6 wff [𝑦 / 𝑥][𝑎 / 𝑦]𝜑
8	7, 5, 2	wsb 2065	. . . . 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  47448  nfich2  47449  ichv  47450  ichf  47451  ichid  47452  icht  47453  ichbidv  47454  ichcircshi  47455  ichan  47456  ichn  47457  dfich2  47459  icheq  47463  ichal  47467  ich2exprop  47472