Theorem nfcvd 2491

Description: If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfcvd	|- (ph -> F/_xA)

Distinct variable group:   x,A

Allowed substitution hint:   ph(x)

Proof of Theorem nfcvd

Step	Hyp	Ref	Expression
1		nfcv 2490	. 2 |- F/_xA
2	1	a1i 10	1 |- (ph -> F/_xA)

This proof depends on syntax axioms:   -> wi 4   F/_wnfc 2477

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-17 1616

This proof depends on definitions:  df-bi 177  df-nf 1545  df-nfc 2479

This theorem is used by:  nfeld  2505  ralcom2  2776  vtoclgft  2906  vtocld  2908  sbcralt  3119  sbcrext  3120  csbied  3179  csbie2t  3181  sbcco3g  3192  csbco3g  3194  dfnfc2  3910  nfiotad  4343  iota2d  4367  iota2  4368  dfid3  4769  oprabid  5551