Theorem nfcvd 2908

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 2907	. 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 1798  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787  df-nfc 2889

This theorem is referenced by:  nfeld  2918  nfraldwOLD  3149  ralcom2  3290  nfreuwOLD  3306  nfrmowOLD  3307  vtoclgft  3492  vtocldOLD  3495  sbcralt  3805  sbcrext  3806  csbiedOLD  3871  csbie2t  3873  sbcco3gw  4356  sbcco3g  4361  csbco3g  4362  dfnfc2  4863  nfdisjw  5051  eusvnfb  5316  eusv2i  5317  dfid3  5492  iota2d  6421  iota2  6422  fmptcof  7002  nfriotadw  7240  riotaeqimp  7259  riota5f  7261  riota5  7262  oprabid  7307  opiota  7899  fmpoco  7935  nfttrcld  9468  axrepndlem1  10348  axrepndlem2  10349  axunnd  10352  axpowndlem2  10354  axpowndlem3  10355  axpowndlem4  10356  axpownd  10357  axregndlem2  10359  axinfndlem1  10361  axinfnd  10362  axacndlem4  10366  axacndlem5  10367  axacnd  10368  nfnegd  11216  prodsn  15672  fprodeq0g  15704  bpolylem  15758  pcmpt  16593  chfacfpmmulfsupp  22012  elmptrab  22978  dvfsumrlim3  25197  itgsubstlem  25212  itgsubst  25213  ifeqeqx  30885  disjunsn  30933  bj-elgab  35127  bj-gabima  35128  unirep  35871  riotasv2d  36971  cdleme31so  38393  cdleme31se  38396  cdleme31sc  38398  cdleme31sde  38399  cdleme31sn2  38403  cdlemeg47rv2  38524  cdlemk41  38934  mapdheq  39742  hdmap1eq  39815  hdmapval2lem  39845  monotuz  40763  oddcomabszz  40766  mnringvald  41826  nfxnegd  42981  fprodsplit1  43134  dvnmul  43484  sge0sn  43917  hoidmvlelem3  44135