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

Metamath Proof Explorer

Theorem nfsbcd

Description: Deduction version of nfsbc . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfsbcdw when possible. (Contributed by NM, 23-Nov-2005) (Revised by Mario Carneiro, 12-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfsbcd.1	$⊢ Ⅎ y φ$
	nfsbcd.2	$⊢ φ \to \underline{Ⅎ} x A$
	nfsbcd.3	$⊢ φ \to Ⅎ x ψ$
Assertion	nfsbcd	$⊢ φ \to Ⅎ x \underset{˙}{[} A / y \underset{˙}{]} ψ$

Proof

Step	Hyp	Ref	Expression
1		nfsbcd.1	$⊢ Ⅎ y φ$
2		nfsbcd.2	$⊢ φ \to \underline{Ⅎ} x A$
3		nfsbcd.3	$⊢ φ \to Ⅎ x ψ$
4		df-sbc	$⊢ \underset{˙}{[} A / y \underset{˙}{]} ψ \leftrightarrow A \in \{y \| ψ\}$
5	1 3	nfabd	$⊢ φ \to \underline{Ⅎ} x \{y \| ψ\}$
6	2 5	nfeld	$⊢ φ \to Ⅎ x A \in \{y \| ψ\}$
7	4 6	nfxfrd	$⊢ φ \to Ⅎ x \underset{˙}{[} A / y \underset{˙}{]} ψ$