Theorem nfcvd 2920

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

Syntax hints:   → wi 4  Ⅎwnfc 2899

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

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786  df-nfc 2901

This theorem is referenced by:  nfeld  2930  nfraldw  3151  ralcom2  3281  nfreuw  3292  nfrmow  3293  vtoclgft  3472  vtoclgftOLD  3473  vtocldOLD  3476  sbcralt  3780  sbcrext  3781  csbied  3843  csbie2t  3845  sbcco3gw  4322  sbcco3g  4327  csbco3g  4328  dfnfc2  4825  nfdisjw  5012  eusvnfb  5265  eusv2i  5266  dfid3  5435  iota2d  6327  iota2  6328  fmptcof  6888  nfriotadw  7121  riotaeqimp  7139  riota5f  7141  riota5  7142  oprabid  7187  opiota  7766  fmpoco  7800  axrepndlem1  10057  axrepndlem2  10058  axunnd  10061  axpowndlem2  10063  axpowndlem3  10064  axpowndlem4  10065  axpownd  10066  axregndlem2  10068  axinfndlem1  10070  axinfnd  10071  axacndlem4  10075  axacndlem5  10076  axacnd  10077  nfnegd  10924  prodsn  15369  fprodeq0g  15401  bpolylem  15455  pcmpt  16288  chfacfpmmulfsupp  21568  elmptrab  22532  dvfsumrlim3  24737  itgsubstlem  24752  itgsubst  24753  ifeqeqx  30412  disjunsn  30460  unirep  35457  riotasv2d  36559  cdleme31so  37981  cdleme31se  37984  cdleme31sc  37986  cdleme31sde  37987  cdleme31sn2  37991  cdlemeg47rv2  38112  cdlemk41  38522  mapdheq  39330  hdmap1eq  39403  hdmapval2lem  39433  monotuz  40283  oddcomabszz  40286  mnringvald  41322  nfxnegd  42472  fprodsplit1  42629  dvnmul  42979  sge0sn  43412  hoidmvlelem3  43630