Theorem nfcvd 2586

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

Syntax hints:   -> wi 4   F/_wnfc 2571

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

This theorem depends on definitions:  df-bi 189  df-nf 1665  df-nfc 2573

This theorem is referenced by:  nfeld  2593  ralcom2  2994  vtoclgft  3130  vtocld  3132  sbcralt  3373  sbcrext  3374  csbied  3423  csbie2t  3425  sbcco3g  3817  csbco3g  3818  dfnfc2  4235  eusvnfb  4618  eusv2i  4619  dfid3  4767  nfiotad  5566  iota2d  5588  iota2  5589  fmptcof  6070  riota5f  6289  riota5  6290  oprabid  6330  opiota  6864  fmpt2co  6888  axrepndlem1  9019  axrepndlem2  9020  axunnd  9023  axpowndlem2  9025  axpowndlem3  9026  axpowndlem4  9027  axpownd  9028  axregndlem2  9030  axinfndlem1  9032  axinfnd  9033  axacndlem4  9037  axacndlem5  9038  axacnd  9039  nfnegd  9872  sumsn  13800  prodsn  14009  fprodeq0g  14041  bpolylem  14094  pcmpt  14830  chfacfpmmulfsupp  19879  elmptrab  20834  dvfsumrlim3  22977  itgsubstlem  22992  itgsubst  22993  ifeqeqx  28154  disjunsn  28200  unirep  31997  riotasv2d  32492  cdleme31so  33909  cdleme31se  33912  cdleme31sc  33914  cdleme31sde  33915  cdleme31sn2  33919  cdlemeg47rv2  34040  cdlemk41  34450  mapdheq  35259  hdmap1eq  35333  hdmapval2lem  35365  monotuz  35753  oddcomabszz  35756  fprodsplit1  37537  dvnmul  37682  sge0sn  38053