Theorem nfcsb1

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

	Ref	Expression
Hypothesis	nfcsb1.1	⊢ Ⅎ 𝑥 𝐴
Assertion	nfcsb1	⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐵

Proof

Step	Hyp	Ref	Expression
1		nfcsb1.1	⊢ Ⅎ 𝑥 𝐴
2	1	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝐴 )
3	2	nfcsb1d	⊢ ( ⊤ → Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
4	3	mptru	⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐵