Theorem nfcvd 2630

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

Syntax hints:   -> wi 4   F/_wnfc 2615

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

This theorem depends on definitions:  df-bi 185  df-nf 1600  df-nfc 2617

This theorem is referenced by:  nfeld  2637  ralcom2  3026  vtoclgft  3161  vtocld  3163  sbcralt  3412  sbcrextOLD  3413  sbcrext  3414  csbied  3462  csbie2t  3464  sbcco3g  3843  csbco3g  3844  dfnfc2  4263  eusvnfb  4643  eusv2i  4644  dfid3  4796  nfiotad  5554  iota2d  5576  iota2  5577  fmptcof  6055  riota5f  6270  riota5  6271  oprabid  6308  opiota  6843  fmpt2co  6866  axrepndlem1  8967  axrepndlem2  8968  axunnd  8971  axpowndlem2  8973  axpowndlem2OLD  8974  axpowndlem3  8975  axpowndlem3OLD  8976  axpowndlem4  8977  axpownd  8978  axregndlem2  8980  axinfndlem1  8983  axinfnd  8984  axacndlem4  8988  axacndlem5  8989  axacnd  8990  nfnegd  9815  sumsn  13526  pcmpt  14270  chfacfpmmulfsupp  19159  elmptrab  20091  dvfsumrlim3  22197  itgsubstlem  22212  itgsubst  22213  ifeqeqx  27121  disjunsn  27154  prodsn  28697  bpolylem  29415  unirep  29834  monotuz  30509  oddcomabszz  30512  riotasv2d  33778  cdleme31so  35193  cdleme31se  35196  cdleme31sc  35198  cdleme31sde  35199  cdleme31sn2  35203  cdlemeg47rv2  35324  cdlemk41  35734  mapdheq  36543  hdmap1eq  36617  hdmapval2lem  36649