Theorem nfcvd 2904

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

Syntax hints:   → wi 4  Ⅎwnfc 2883

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

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786  df-nfc 2885

This theorem is referenced by:  nfeld  2914  nfraldwOLD  3318  ralcom2  3373  nfreuwOLD  3422  nfrmowOLD  3423  vtoclgft  3540  vtocldOLD  3543  sbcralt  3865  sbcrext  3866  csbiedOLD  3931  csbie2t  3933  sbcco3gw  4421  sbcco3g  4426  csbco3g  4427  dfnfc2  4932  nfdisjw  5124  eusvnfb  5390  eusv2i  5391  dfid3  5576  iota2d  6528  iota2  6529  fmptcof  7124  nfriotadw  7369  riotaeqimp  7388  riota5f  7390  riota5  7391  oprabid  7437  opiota  8041  fmpoco  8077  nfttrcld  9701  axrepndlem1  10583  axrepndlem2  10584  axunnd  10587  axpowndlem2  10589  axpowndlem3  10590  axpowndlem4  10591  axpownd  10592  axregndlem2  10594  axinfndlem1  10596  axinfnd  10597  axacndlem4  10601  axacndlem5  10602  axacnd  10603  nfnegd  11451  prodsn  15902  fprodeq0g  15934  bpolylem  15988  pcmpt  16821  chfacfpmmulfsupp  22356  elmptrab  23322  dvfsumrlim3  25541  itgsubstlem  25556  itgsubst  25557  ifeqeqx  31761  disjunsn  31812  bj-elgab  35807  bj-gabima  35808  wl-issetft  36432  unirep  36570  riotasv2d  37815  cdleme31so  39238  cdleme31se  39241  cdleme31sc  39243  cdleme31sde  39244  cdleme31sn2  39248  cdlemeg47rv2  39369  cdlemk41  39779  mapdheq  40587  hdmap1eq  40660  hdmapval2lem  40690  monotuz  41665  oddcomabszz  41668  mnringvald  42952  nfxnegd  44137  fprodsplit1  44295  dvnmul  44645  sge0sn  45081  hoidmvlelem3  45299