Theorem nfcsb1d

Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016)

	Ref	Expression
Hypothesis	nfcsb1d.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion	nfcsb1d	⊢ ( 𝜑 → Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfcsb1d.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }
3		nfv	⊢ Ⅎ 𝑦 𝜑
4	1	nfsbc1d	⊢ ( 𝜑 → Ⅎ 𝑥 [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 )
5	3 4	nfabdw	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } )
6	2 5	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )