ichf

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

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

Metamath Proof Explorer