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

Metamath Proof Explorer

Theorem sbcbidv

Description: Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014) Drop ax-12 . (Revised by GG, 1-Dec-2023)

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

Step	Hyp	Ref	Expression
1		sbcbidv.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		eqidd	$⊢ φ \to A = A$
3	2 1	sbceqbid	$⊢ φ \to (\underset{˙}{[} A / x \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} χ)$