Theorem nfcvd 2895

Description: If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfcvd	⊢ (𝜑 → Ⅎ𝑥𝐴)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfcvd

Step	Hyp	Ref	Expression
1		nfcv 2894	. 2 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	1 ⊢ (𝜑 → Ⅎ𝑥𝐴)

Syntax hints:   → wi 4  Ⅎwnfc 2879

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

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785  df-nfc 2881

This theorem is referenced by:  nfeld  2906  ralcom2  3343  cbvexeqsetf  3451  sbcralt  3823  sbcrext  3824  csbie2t  3888  sbcco3gw  4375  sbcco3g  4380  csbco3g  4381  dfnfc2  4881  nfdisjw  5070  eusvnfb  5331  eusv2i  5332  dfid3  5514  iota2d  6469  iota2  6470  fmptcof  7063  nfriotadw  7311  riotaeqimp  7329  riota5f  7331  riota5  7332  oprabid  7378  opiota  7991  fmpoco  8025  nfttrcld  9600  axrepndlem1  10480  axrepndlem2  10481  axunnd  10484  axpowndlem2  10486  axpowndlem3  10487  axpowndlem4  10488  axpownd  10489  axregndlem2  10491  axinfndlem1  10493  axinfnd  10494  axacndlem4  10498  axacndlem5  10499  axacnd  10500  nfnegd  11352  prodsn  15866  fprodeq0g  15898  bpolylem  15952  pcmpt  16801  nfchnd  18514  chfacfpmmulfsupp  22776  elmptrab  23740  dvfsumrlim3  25965  itgsubstlem  25980  itgsubst  25981  ifeqeqx  32517  disjunsn  32569  axnulg  35110  bj-elgab  36972  bj-gabima  36973  wl-issetft  37615  unirep  37753  riotasv2d  38995  cdleme31so  40417  cdleme31se  40420  cdleme31sc  40422  cdleme31sde  40423  cdleme31sn2  40427  cdlemeg47rv2  40548  cdlemk41  40958  mapdheq  41766  hdmap1eq  41839  hdmapval2lem  41869  monotuz  42973  oddcomabszz  42976  mnringvald  44245  nfxnegd  45478  fprodsplit1  45632  dvnmul  45980  sge0sn  46416  hoidmvlelem3  46634