df-ich

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

		Ref	Expression
	Assertion	df-ich	$⊢ [x ⇄ y] φ \leftrightarrow \forall x \forall y ([x/ a] [y/ x] [a/ y] φ \leftrightarrow φ)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$setvar x$
1		vy	$setvar y$
2		wph	$wff φ$
3	2 0 1	wich	$wff [x ⇄ y] φ$
4		va	$setvar a$
5	2 1 4	wsb	$wff [a/ y] φ$
6	5 0 1	wsb	$wff [y/ x] [a/ y] φ$
7	6 4 0	wsb	$wff [x/ a] [y/ x] [a/ y] φ$
8	7 2	wb	$wff ([x/ a] [y/ x] [a/ y] φ \leftrightarrow φ)$
9	8 1	wal	$wff \forall y ([x/ a] [y/ x] [a/ y] φ \leftrightarrow φ)$
10	9 0	wal	$wff \forall x \forall y ([x/ a] [y/ x] [a/ y] φ \leftrightarrow φ)$
11	3 10	wb	$wff ([x ⇄ y] φ \leftrightarrow \forall x \forall y ([x/ a] [y/ x] [a/ y] φ \leftrightarrow φ))$

Metamath Proof Explorer

Definition df-ich

Detailed syntax breakdown