Theorem nfcvd 2570

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

Syntax hints:   -> wi 4   F/_wnfc 2556

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

This theorem depends on definitions:  df-bi 185  df-nf 1593  df-nfc 2558

This theorem is referenced by:  nfeld  2584  ralcom2  2875  vtoclgft  3009  vtocld  3011  sbcralt  3255  sbcrextOLD  3256  sbcrext  3257  csbied  3302  csbie2t  3304  sbcco3g  3683  csbco3g  3684  dfnfc2  4097  eusvnfb  4476  eusv2i  4477  dfid3  4624  nfiotad  5372  iota2d  5394  iota2  5395  fmptcof  5864  riota5f  6065  riota5  6066  oprabid  6104  opiota  6622  fmpt2co  6645  axrepndlem1  8744  axrepndlem2  8745  axunnd  8748  axpowndlem2  8750  axpowndlem2OLD  8751  axpowndlem3  8752  axpowndlem3OLD  8753  axpowndlem4  8754  axpownd  8755  axregndlem2  8757  axinfndlem1  8759  axinfnd  8760  axacndlem4  8764  axacndlem5  8765  axacnd  8766  nfnegd  9592  sumsn  13200  pcmpt  13936  elmptrab  19241  dvfsumrlim3  21346  itgsubstlem  21361  itgsubst  21362  ifeqeqx  25725  disjunsn  25759  prodsn  27319  bpolylem  28037  unirep  28447  monotuz  29124  oddcomabszz  29127  riotasv2d  32178  cdleme31so  33593  cdleme31se  33596  cdleme31sc  33598  cdleme31sde  33599  cdleme31sn2  33603  cdlemeg47rv2  33724  cdlemk41  34134  mapdheq  34943  hdmap1eq  35017  hdmapval2lem  35049