Theorem nfcvd 2905

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

Syntax hints:   → wi 4  Ⅎwnfc 2884

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

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

This theorem is referenced by:  nfeld  2915  nfraldwOLD  3319  ralcom2  3374  nfreuwOLD  3423  nfrmowOLD  3424  vtoclgft  3541  vtocldOLD  3544  sbcralt  3867  sbcrext  3868  csbiedOLD  3933  csbie2t  3935  sbcco3gw  4423  sbcco3g  4428  csbco3g  4429  dfnfc2  4934  nfdisjw  5126  eusvnfb  5392  eusv2i  5393  dfid3  5578  iota2d  6532  iota2  6533  fmptcof  7128  nfriotadw  7373  riotaeqimp  7392  riota5f  7394  riota5  7395  oprabid  7441  opiota  8045  fmpoco  8081  nfttrcld  9705  axrepndlem1  10587  axrepndlem2  10588  axunnd  10591  axpowndlem2  10593  axpowndlem3  10594  axpowndlem4  10595  axpownd  10596  axregndlem2  10598  axinfndlem1  10600  axinfnd  10601  axacndlem4  10605  axacndlem5  10606  axacnd  10607  nfnegd  11455  prodsn  15906  fprodeq0g  15938  bpolylem  15992  pcmpt  16825  chfacfpmmulfsupp  22365  elmptrab  23331  dvfsumrlim3  25550  itgsubstlem  25565  itgsubst  25566  ifeqeqx  31774  disjunsn  31825  bj-elgab  35819  bj-gabima  35820  wl-issetft  36444  unirep  36582  riotasv2d  37827  cdleme31so  39250  cdleme31se  39253  cdleme31sc  39255  cdleme31sde  39256  cdleme31sn2  39260  cdlemeg47rv2  39381  cdlemk41  39791  mapdheq  40599  hdmap1eq  40672  hdmapval2lem  40702  monotuz  41680  oddcomabszz  41683  mnringvald  42967  nfxnegd  44151  fprodsplit1  44309  dvnmul  44659  sge0sn  45095  hoidmvlelem3  45313