Theorem nfcvd 2595

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 2594	. 2 |- F/_ x A
2	1	a1i 11	1 |- ( ph -> F/_ x A )

Syntax hints:   -> wi 4   F/_wnfc 2581

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

This theorem depends on definitions:  df-bi 189  df-nf 1670  df-nfc 2583

This theorem is referenced by:  nfeld  2602  ralcom2  2957  vtoclgft  3098  vtocld  3100  sbcralt  3342  sbcrext  3343  csbied  3392  csbie2t  3394  sbcco3g  3790  csbco3g  3791  dfnfc2  4219  eusvnfb  4602  eusv2i  4603  dfid3  4753  nfiotad  5552  iota2d  5574  iota2  5575  fmptcof  6062  riota5f  6281  riota5  6282  oprabid  6322  opiota  6857  fmpt2co  6884  axrepndlem1  9022  axrepndlem2  9023  axunnd  9026  axpowndlem2  9028  axpowndlem3  9029  axpowndlem4  9030  axpownd  9031  axregndlem2  9033  axinfndlem1  9035  axinfnd  9036  axacndlem4  9040  axacndlem5  9041  axacnd  9042  nfnegd  9875  sumsn  13819  prodsn  14028  fprodeq0g  14060  bpolylem  14113  pcmpt  14849  chfacfpmmulfsupp  19899  elmptrab  20854  dvfsumrlim3  22997  itgsubstlem  23012  itgsubst  23013  ifeqeqx  28170  disjunsn  28216  unirep  32051  riotasv2d  32541  cdleme31so  33958  cdleme31se  33961  cdleme31sc  33963  cdleme31sde  33964  cdleme31sn2  33968  cdlemeg47rv2  34089  cdlemk41  34499  mapdheq  35308  hdmap1eq  35382  hdmapval2lem  35414  monotuz  35801  oddcomabszz  35804  fprodsplit1  37683  dvnmul  37828  sge0sn  38231  hoidmvlelem3  38429  riotaeqimp  39047