Definition df-ich 47476

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 47484. Another, equivalent definition using two temporary setvar variables is provided in dfich2 47488. (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 47475	. 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 206	. . . 4 wff ([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)
10	9, 3	wal 1539	. . 3 wff ∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)
11	10, 2	wal 1539	. 2 wff ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)
12	4, 11	wb 206	1 wff ([𝑥⇄𝑦]𝜑 ↔ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑))

This definition is referenced by:  nfich1  47477  nfich2  47478  ichv  47479  ichf  47480  ichid  47481  icht  47482  ichbidv  47483  ichcircshi  47484  ichan  47485  ichn  47486  dfich2  47488  icheq  47492  ichal  47496  ich2exprop  47501