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 ⊢ Ⅎ _ x A
Assertion nfcsb1 ⊢ Ⅎ _ x ⦋ A / x⦌ B

Proof

Step Hyp Ref Expression
1 nfcsb1.1 ⊢ Ⅎ _ x A
2 1 a1i ⊢ ⊤ → Ⅎ _ x A
3 2 nfcsb1d ⊢ ⊤ → Ⅎ _ x ⦋ A / x⦌ B
4 3 mptru ⊢ Ⅎ _ x ⦋ A / x⦌ B