Theorem nfcvd 2903

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 2902	. 2 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	1 ⊢ (𝜑 → Ⅎ𝑥𝐴)

Syntax hints:   → wi 4  Ⅎwnfc 2887

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

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791  df-nfc 2889

This theorem is referenced by:  nfeld  2913  ralcom2  3342  cbvexeqsetf  3447  sbcralt  3811  sbcrext  3812  csbie2t  3876  sbcco3gw  4360  sbcco3g  4365  csbco3g  4366  dfnfc2  4867  eusvnfb  5329  eusv2i  5330  dfid3  5523  iota2d  6480  iota2  6481  fmptcof  7079  nfriotadw  7328  riotaeqimp  7346  riota5f  7348  riota5  7349  oprabid  7395  opiota  8008  fmpoco  8041  nfttrcld  9629  axrepndlem1  10513  axrepndlem2  10514  axunnd  10517  axpowndlem2  10519  axpowndlem3  10520  axpowndlem4  10521  axpownd  10522  axregndlem2  10524  axinfndlem1  10526  axinfnd  10527  axacndlem4  10531  axacndlem5  10532  axacnd  10533  nfnegd  11386  prodsn  15925  fprodeq0g  15957  bpolylem  16011  pcmpt  16861  nfchnd  18575  chfacfpmmulfsupp  22853  elmptrab  23817  dvfsumrlim3  26025  itgsubstlem  26040  itgsubst  26041  ifeqeqx  32637  disjunsn  32690  axsepg2  35328  axnulg  35333  axpowg2  35335  axpowg3  35336  bj-elgab  37299  bj-gabima  37300  wl-issetft  37960  unirep  38088  riotasv2d  39456  cdleme31so  40878  cdleme31se  40881  cdleme31sc  40883  cdleme31sde  40884  cdleme31sn2  40888  cdlemeg47rv2  41009  cdlemk41  41419  mapdheq  42227  hdmap1eq  42300  hdmapval2lem  42330  monotuz  43393  oddcomabszz  43396  mnringvald  44664  nfxnegd  45891  fprodsplit1  46045  dvnmul  46393  sge0sn  46829  hoidmvlelem3  47047