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

Metamath Proof Explorer

Theorem nfsbcdw

Description: Deduction version of nfsbcw . Version of nfsbcd with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 23-Nov-2005) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

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

Proof

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