Theorem nfcvd 2545

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

Syntax hints:   -> wi 4   F/_wnfc 2530

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

This theorem depends on definitions:  df-bi 185  df-nf 1625  df-nfc 2532

This theorem is referenced by:  nfeld  2552  ralcom2  2947  vtoclgft  3082  vtocld  3084  sbcralt  3325  sbcrext  3326  csbied  3375  csbie2t  3377  sbcco3g  3766  csbco3g  3767  dfnfc2  4181  eusvnfb  4561  eusv2i  4562  dfid3  4710  nfiotad  5463  iota2d  5485  iota2  5486  fmptcof  5967  riota5f  6182  riota5  6183  oprabid  6223  opiota  6758  fmpt2co  6782  axrepndlem1  8880  axrepndlem2  8881  axunnd  8884  axpowndlem2  8886  axpowndlem3  8887  axpowndlem4  8888  axpownd  8889  axregndlem2  8891  axinfndlem1  8894  axinfnd  8895  axacndlem4  8899  axacndlem5  8900  axacnd  8901  nfnegd  9728  sumsn  13565  prodsn  13769  pcmpt  14413  chfacfpmmulfsupp  19449  elmptrab  20413  dvfsumrlim3  22519  itgsubstlem  22534  itgsubst  22535  ifeqeqx  27544  disjunsn  27583  bpolylem  29963  unirep  30369  monotuz  31042  oddcomabszz  31045  fprodsplit1  31765  fprodeq0g  31767  dvnmul  31906  riotasv2d  35101  cdleme31so  36518  cdleme31se  36521  cdleme31sc  36523  cdleme31sde  36524  cdleme31sn2  36528  cdlemeg47rv2  36649  cdlemk41  37059  mapdheq  37868  hdmap1eq  37942  hdmapval2lem  37974