Theorem nfcvd 2490

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 2489	. 2 |- F/_xA
2	1	a1i 10	1 |- (ph -> F/_xA)

Syntax hints:   -> wi 4   F/_wnfc 2476

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-17 1616

This theorem depends on definitions:  df-bi 177  df-nf 1545  df-nfc 2478

This theorem is referenced by:  nfeld  2504  ralcom2  2775  vtoclgft  2905  vtocld  2907  sbcralt  3118  sbcrext  3119  csbied  3178  csbie2t  3180  sbcco3g  3191  csbco3g  3193  dfnfc2  3909  nfiotad  4342  iota2d  4366  iota2  4367  dfid3  4768  oprabid  5550