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

Proof

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