ichv

Description: Setvar variables are interchangeable in a wff they do not appear in. (Contributed by SN, 23-Nov-2023)

		Ref	Expression
	Assertion	ichv	$⊢ [x ⇄ y] φ$

Step	Hyp	Ref	Expression
1		sbv	$⊢ [a/ y] φ \leftrightarrow φ$
2	1	sbbii	$⊢ [y/ x] [a/ y] φ \leftrightarrow [y/ x] φ$
3		sbv	$⊢ [y/ x] φ \leftrightarrow φ$
4	2 3	bitri	$⊢ [y/ x] [a/ y] φ \leftrightarrow φ$
5	4	sbbii	$⊢ [x/ a] [y/ x] [a/ y] φ \leftrightarrow [x/ a] φ$
6		sbv	$⊢ [x/ a] φ \leftrightarrow φ$
7	5 6	bitri	$⊢ [x/ a] [y/ x] [a/ y] φ \leftrightarrow φ$
8	7	gen2	$⊢ \forall x \forall y ([x/ a] [y/ x] [a/ y] φ \leftrightarrow φ)$
9		df-ich	$⊢ [x ⇄ y] φ \leftrightarrow \forall x \forall y ([x/ a] [y/ x] [a/ y] φ \leftrightarrow φ)$
10	8 9	mpbir	$⊢ [x ⇄ y] φ$

Metamath Proof Explorer