This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfsbc1d

Description: Deduction version of nfsbc1 . (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 12-Oct-2016)

Ref Expression
Hypothesis nfsbc1d.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion nfsbc1d ( 𝜑 → Ⅎ 𝑥 [ 𝐴 / 𝑥 ] 𝜓 )

Proof

Step Hyp Ref Expression
1 nfsbc1d.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2 df-sbc ⊢ ( [ 𝐴 / 𝑥 ] 𝜓 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜓 } )
3 nfab1 ⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜓 }
4 3 a1i ⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑥 ∣ 𝜓 } )
5 1 4 nfeld ⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 ∈ { 𝑥 ∣ 𝜓 } )
6 2 5 nfxfrd ⊢ ( 𝜑 → Ⅎ 𝑥 [ 𝐴 / 𝑥 ] 𝜓 )