Theorem nfcvd 2606

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/_ x A )

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem nfcvd

Step	Hyp	Ref	Expression
1		nfcv 2605	. 2 |- F/_ x A
2	1	a1i 11	1 |- ( ph -> F/_ x A )

Syntax hints:   -> wi 4   F/_wnfc 2591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-5 1691

This theorem depends on definitions:  df-bi 185  df-nf 1604  df-nfc 2593

This theorem is referenced by:  nfeld  2613  ralcom2  3008  vtoclgft  3143  vtocld  3145  sbcralt  3394  sbcrextOLD  3395  sbcrext  3396  csbied  3447  csbie2t  3449  sbcco3g  3829  csbco3g  3830  dfnfc2  4252  eusvnfb  4633  eusv2i  4634  dfid3  4786  nfiotad  5544  iota2d  5566  iota2  5567  fmptcof  6050  riota5f  6267  riota5  6268  oprabid  6308  opiota  6844  fmpt2co  6868  axrepndlem1  8970  axrepndlem2  8971  axunnd  8974  axpowndlem2  8976  axpowndlem2OLD  8977  axpowndlem3  8978  axpowndlem3OLD  8979  axpowndlem4  8980  axpownd  8981  axregndlem2  8983  axinfndlem1  8986  axinfnd  8987  axacndlem4  8991  axacndlem5  8992  axacnd  8993  nfnegd  9820  sumsn  13545  prodsn  13749  pcmpt  14393  chfacfpmmulfsupp  19342  elmptrab  20306  dvfsumrlim3  22412  itgsubstlem  22427  itgsubst  22428  ifeqeqx  27397  disjunsn  27431  bpolylem  29786  unirep  30179  monotuz  30853  oddcomabszz  30856  fprodsplit1  31553  fprodeq0g  31555  dvnmul  31694  riotasv2d  34563  cdleme31so  35980  cdleme31se  35983  cdleme31sc  35985  cdleme31sde  35986  cdleme31sn2  35990  cdlemeg47rv2  36111  cdlemk41  36521  mapdheq  37330  hdmap1eq  37404  hdmapval2lem  37436