Metamath Proof Explorer

Theorem nfsbc1v

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

Ref Expression
Assertion nfsbc1v 
|- F/ x [. A / x ]. ph

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ x A
2 1 nfsbc1 
 |-  F/ x [. A / x ]. ph