Metamath Proof Explorer


Theorem nfcsbd

Description: Deduction version of nfcsb . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 21-Nov-2005) (Revised by Mario Carneiro, 12-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses nfcsbd.1 yφ
nfcsbd.2 φ_xA
nfcsbd.3 φ_xB
Assertion nfcsbd φ_xA/yB

Proof

Step Hyp Ref Expression
1 nfcsbd.1 yφ
2 nfcsbd.2 φ_xA
3 nfcsbd.3 φ_xB
4 df-csb A/yB=z|[˙A/y]˙zB
5 nfv zφ
6 3 nfcrd φxzB
7 1 2 6 nfsbcd φx[˙A/y]˙zB
8 5 7 nfabd φ_xz|[˙A/y]˙zB
9 4 8 nfcxfrd φ_xA/yB