ichcom

Description: The interchangeability of setvar variables is commutative. (Contributed by AV, 20-Aug-2023)

		Ref	Expression
	Assertion	ichcom	$⊢ [x ⇄ y] ψ \leftrightarrow [y ⇄ x] ψ$

Step	Hyp	Ref	Expression
1		alcom	$⊢ \forall b \forall a ([b/ x] [a/ y] ψ \leftrightarrow [a/ x] [b/ y] ψ) \leftrightarrow \forall a \forall b ([b/ x] [a/ y] ψ \leftrightarrow [a/ x] [b/ y] ψ)$
2		sbcom2	$⊢ [b/ x] [a/ y] ψ \leftrightarrow [a/ y] [b/ x] ψ$
3		sbcom2	$⊢ [a/ x] [b/ y] ψ \leftrightarrow [b/ y] [a/ x] ψ$
4	2 3	bibi12i	$⊢ ([b/ x] [a/ y] ψ \leftrightarrow [a/ x] [b/ y] ψ) \leftrightarrow ([a/ y] [b/ x] ψ \leftrightarrow [b/ y] [a/ x] ψ)$
5	4	2albii	$⊢ \forall a \forall b ([b/ x] [a/ y] ψ \leftrightarrow [a/ x] [b/ y] ψ) \leftrightarrow \forall a \forall b ([a/ y] [b/ x] ψ \leftrightarrow [b/ y] [a/ x] ψ)$
6	1 5	bitri	$⊢ \forall b \forall a ([b/ x] [a/ y] ψ \leftrightarrow [a/ x] [b/ y] ψ) \leftrightarrow \forall a \forall b ([a/ y] [b/ x] ψ \leftrightarrow [b/ y] [a/ x] ψ)$
7		dfich2	$⊢ [x ⇄ y] ψ \leftrightarrow \forall b \forall a ([b/ x] [a/ y] ψ \leftrightarrow [a/ x] [b/ y] ψ)$
8		dfich2	$⊢ [y ⇄ x] ψ \leftrightarrow \forall a \forall b ([a/ y] [b/ x] ψ \leftrightarrow [b/ y] [a/ x] ψ)$
9	6 7 8	3bitr4i	$⊢ [x ⇄ y] ψ \leftrightarrow [y ⇄ x] ψ$

Metamath Proof Explorer