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

Metamath Proof Explorer

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 ⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐵