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

Metamath Proof Explorer

Theorem sbceq1a

Description: Equality theorem for class substitution. Class version of sbequ12 . (Contributed by NM, 26-Sep-2003)

		Ref	Expression
	Assertion	sbceq1a	$⊢ x = A \to (φ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} φ)$

Step	Hyp	Ref	Expression
1		sbid	$⊢ [x/ x] φ \leftrightarrow φ$
2		dfsbcq2	$⊢ x = A \to ([x/ x] φ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} φ)$
3	1 2	bitr3id	$⊢ x = A \to (φ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} φ)$