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 𝑥 𝐴
nfsbc.2 𝑥 𝜑
Assertion nfsbc 𝑥 [ 𝐴 / 𝑦 ] 𝜑

Proof

Step Hyp Ref Expression
1 nfsbc.1 𝑥 𝐴
2 nfsbc.2 𝑥 𝜑
3 nftru 𝑦
4 1 a1i ( ⊤ → 𝑥 𝐴 )
5 2 a1i ( ⊤ → Ⅎ 𝑥 𝜑 )
6 3 4 5 nfsbcd ( ⊤ → Ⅎ 𝑥 [ 𝐴 / 𝑦 ] 𝜑 )
7 6 mptru 𝑥 [ 𝐴 / 𝑦 ] 𝜑