Metamath Proof Explorer


Theorem nfsbc

Description: Bound-variable hypothesis builder for class substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfsbcw when possible. (Contributed by NM, 7-Sep-2014) (Revised by Mario Carneiro, 12-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses nfsbc.1
|- F/_ x A
nfsbc.2
|- F/ x ph
Assertion nfsbc
|- F/ x [. A / y ]. ph

Proof

Step Hyp Ref Expression
1 nfsbc.1
 |-  F/_ x A
2 nfsbc.2
 |-  F/ x ph
3 nftru
 |-  F/ y T.
4 1 a1i
 |-  ( T. -> F/_ x A )
5 2 a1i
 |-  ( T. -> F/ x ph )
6 3 4 5 nfsbcd
 |-  ( T. -> F/ x [. A / y ]. ph )
7 6 mptru
 |-  F/ x [. A / y ]. ph