Metamath Proof Explorer

Theorem nfsbcd

Description: Deduction version of nfsbc . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfsbcdw when possible. (Contributed by NM, 23-Nov-2005) (Revised by Mario Carneiro, 12-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses nfsbcd.1 y φ
nfsbcd.2 φ _ x A
nfsbcd.3 φ x ψ
Assertion nfsbcd φ x [˙A / y]˙ ψ


Step Hyp Ref Expression
1 nfsbcd.1 y φ
2 nfsbcd.2 φ _ x A
3 nfsbcd.3 φ x ψ
4 df-sbc [˙A / y]˙ ψ A y | ψ
5 1 3 nfabd φ _ x y | ψ
6 2 5 nfeld φ x A y | ψ
7 4 6 nfxfrd φ x [˙A / y]˙ ψ