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

Metamath Proof Explorer

Theorem sbequ12a

Description: An equality theorem for substitution. (Contributed by NM, 2-Jun-1993) (Proof shortened by Wolf Lammen, 23-Jun-2019)

		Ref	Expression
	Assertion	sbequ12a	$⊢ x = y \to ([y/ x] φ \leftrightarrow [x/ y] φ)$

Step	Hyp	Ref	Expression
1		sbequ12r	$⊢ x = y \to ([x/ y] φ \leftrightarrow φ)$
2		sbequ12	$⊢ x = y \to (φ \leftrightarrow [y/ x] φ)$
3	1 2	bitr2d	$⊢ x = y \to ([y/ x] φ \leftrightarrow [x/ y] φ)$