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	⊢ Ⅎ 𝑦 𝜑
	nfsbcdw.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
	nfsbcdw.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
Assertion	nfsbcdw	⊢ ( 𝜑 → Ⅎ 𝑥 [ 𝐴 / 𝑦 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nfsbcdw.1	⊢ Ⅎ 𝑦 𝜑
2		nfsbcdw.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
3		nfsbcdw.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
4		df-sbc	⊢ ( [ 𝐴 / 𝑦 ] 𝜓 ↔ 𝐴 ∈ { 𝑦 ∣ 𝜓 } )
5	1 3	nfabdw	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑦 ∣ 𝜓 } )
6	2 5	nfeld	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 ∈ { 𝑦 ∣ 𝜓 } )
7	4 6	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 [ 𝐴 / 𝑦 ] 𝜓 )