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

Metamath Proof Explorer

Theorem sbcied2

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014)

	Ref	Expression
Hypotheses	sbcied2.1	$⊢ φ \to A \in V$
	sbcied2.2	$⊢ φ \to A = B$
	sbcied2.3	$⊢ (φ \land x = B) \to (ψ \leftrightarrow χ)$
Assertion	sbcied2	$⊢ φ \to (\underset{˙}{[} A / x \underset{˙}{]} ψ \leftrightarrow χ)$

Step	Hyp	Ref	Expression
1		sbcied2.1	$⊢ φ \to A \in V$
2		sbcied2.2	$⊢ φ \to A = B$
3		sbcied2.3	$⊢ (φ \land x = B) \to (ψ \leftrightarrow χ)$
4		id	$⊢ x = A \to x = A$
5	4 2	sylan9eqr	$⊢ (φ \land x = A) \to x = B$
6	5 3	syldan	$⊢ (φ \land x = A) \to (ψ \leftrightarrow χ)$
7	1 6	sbcied	$⊢ φ \to (\underset{˙}{[} A / x \underset{˙}{]} ψ \leftrightarrow χ)$