Definition df-ich 46780

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

This definition is referenced by:  nfich1  46781  nfich2  46782  ichv  46783  ichf  46784  ichid  46785  icht  46786  ichbidv  46787  ichcircshi  46788  ichan  46789  ichn  46790  dfich2  46792  icheq  46796  ichal  46800  ich2exprop  46805