sbcbid

Description: Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014)

	Ref	Expression
Hypotheses	sbcbid.1	$⊢ Ⅎ x φ$
	sbcbid.2	$⊢ φ \to (ψ \leftrightarrow χ)$
Assertion	sbcbid	$⊢ φ \to (\underset{˙}{[} A / x \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} χ)$

Step	Hyp	Ref	Expression
1		sbcbid.1	$⊢ Ⅎ x φ$
2		sbcbid.2	$⊢ φ \to (ψ \leftrightarrow χ)$
3	1 2	abbid	$⊢ φ \to \{x \| ψ\} = \{x \| χ\}$
4	3	eleq2d	$⊢ φ \to (A \in \{x \| ψ\} \leftrightarrow A \in \{x \| χ\})$
5		df-sbc	$⊢ \underset{˙}{[} A / x \underset{˙}{]} ψ \leftrightarrow A \in \{x \| ψ\}$
6		df-sbc	$⊢ \underset{˙}{[} A / x \underset{˙}{]} χ \leftrightarrow A \in \{x \| χ\}$
7	4 5 6	3bitr4g	$⊢ φ \to (\underset{˙}{[} A / x \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} χ)$

Metamath Proof Explorer