Theorem nfcvd 2615

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

Syntax hints:   -> wi 4   F/_wnfc 2600

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

This theorem depends on definitions:  df-bi 185  df-nf 1591  df-nfc 2602

This theorem is referenced by:  nfeld  2622  ralcom2  2985  vtoclgft  3120  vtocld  3122  sbcralt  3369  sbcrextOLD  3370  sbcrext  3371  csbied  3417  csbie2t  3419  sbcco3g  3798  csbco3g  3799  dfnfc2  4212  eusvnfb  4591  eusv2i  4592  dfid3  4740  nfiotad  5487  iota2d  5509  iota2  5510  fmptcof  5981  riota5f  6181  riota5  6182  oprabid  6219  opiota  6738  fmpt2co  6761  axrepndlem1  8862  axrepndlem2  8863  axunnd  8866  axpowndlem2  8868  axpowndlem2OLD  8869  axpowndlem3  8870  axpowndlem3OLD  8871  axpowndlem4  8872  axpownd  8873  axregndlem2  8875  axinfndlem1  8878  axinfnd  8879  axacndlem4  8883  axacndlem5  8884  axacnd  8885  nfnegd  9711  sumsn  13330  pcmpt  14067  elmptrab  19527  dvfsumrlim3  21633  itgsubstlem  21648  itgsubst  21649  ifeqeqx  26049  disjunsn  26082  prodsn  27612  bpolylem  28330  unirep  28749  monotuz  29425  oddcomabszz  29428  chfacfpmmulfsupp  31330  riotasv2d  32927  cdleme31so  34342  cdleme31se  34345  cdleme31sc  34347  cdleme31sde  34348  cdleme31sn2  34352  cdlemeg47rv2  34473  cdlemk41  34883  mapdheq  35692  hdmap1eq  35766  hdmapval2lem  35798