Metamath Proof Explorer


Theorem nfsbc1

Description: Bound-variable hypothesis builder for class substitution. (Contributed by NM, 5-Aug-1993) (Revised by Mario Carneiro, 12-Oct-2016)

Ref Expression
Hypothesis nfsbc1.1
|- F/_ x A
Assertion nfsbc1
|- F/ x [. A / x ]. ph

Proof

Step Hyp Ref Expression
1 nfsbc1.1
 |-  F/_ x A
2 1 a1i
 |-  ( T. -> F/_ x A )
3 2 nfsbc1d
 |-  ( T. -> F/ x [. A / x ]. ph )
4 3 mptru
 |-  F/ x [. A / x ]. ph