ichid

Description: A setvar variable is always interchangeable with itself. (Contributed by AV, 29-Jul-2023)

		Ref	Expression
	Assertion	ichid	$⊢ [x ⇄ x] φ$

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

Metamath Proof Explorer