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

Metamath Proof Explorer

Theorem eqsb1

Description: Substitution for the left-hand side in an equality. Class version of equsb3 . (Contributed by Rodolfo Medina, 28-Apr-2010)

		Ref	Expression
	Assertion	eqsb1	$⊢ [y/ x] x = A \leftrightarrow y = A$

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ x = w \to (x = A \leftrightarrow w = A)$
2		eqeq1	$⊢ w = y \to (w = A \leftrightarrow y = A)$
3	1 2	sbievw2	$⊢ [y/ x] x = A \leftrightarrow y = A$