This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem icht

Description: A theorem is interchangeable. (Contributed by SN, 4-May-2024)

		Ref	Expression
	Hypothesis	icht.1	$⊢ φ$
	Assertion	icht	$⊢ [x ⇄ y] φ$

Step	Hyp	Ref	Expression
1		icht.1	$⊢ φ$
2	1	sbt	$⊢ [a/ y] φ$
3	2	sbt	$⊢ [y/ x] [a/ y] φ$
4	3	sbt	$⊢ [x/ a] [y/ x] [a/ y] φ$
5	4 1	2th	$⊢ [x/ a] [y/ x] [a/ y] φ \leftrightarrow φ$
6	5	gen2	$⊢ \forall x \forall y ([x/ a] [y/ x] [a/ y] φ \leftrightarrow φ)$
7		df-ich	$⊢ [x ⇄ y] φ \leftrightarrow \forall x \forall y ([x/ a] [y/ x] [a/ y] φ \leftrightarrow φ)$
8	6 7	mpbir	$⊢ [x ⇄ y] φ$