Theorem nfcvd 2765

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

Syntax hints:   → wi 4  Ⅎwnfc 2751

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

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710  df-nfc 2753

This theorem is referenced by:  nfeld  2773  ralcom2  3104  vtoclgft  3254  vtoclgftOLD  3255  vtocld  3257  sbcralt  3510  sbcrext  3511  sbcrextOLD  3512  csbied  3560  csbie2t  3562  sbcco3g  3999  csbco3g  4000  dfnfc2  4454  dfnfc2OLD  4455  eusvnfb  4862  eusv2i  4863  dfid3  5025  iota2d  5876  iota2  5877  fmptcof  6397  riotaeqimp  6634  riota5f  6636  riota5  6637  oprabid  6677  opiota  7229  fmpt2co  7260  axrepndlem1  9414  axrepndlem2  9415  axunnd  9418  axpowndlem2  9420  axpowndlem3  9421  axpowndlem4  9422  axpownd  9423  axregndlem2  9425  axinfndlem1  9427  axinfnd  9428  axacndlem4  9432  axacndlem5  9433  axacnd  9434  nfnegd  10276  sumsn  14475  prodsn  14692  fprodeq0g  14725  bpolylem  14779  pcmpt  15596  chfacfpmmulfsupp  20668  elmptrab  21630  dvfsumrlim3  23796  itgsubstlem  23811  itgsubst  23812  ifeqeqx  29361  disjunsn  29407  unirep  33507  riotasv2d  34243  cdleme31so  35667  cdleme31se  35670  cdleme31sc  35672  cdleme31sde  35673  cdleme31sn2  35677  cdlemeg47rv2  35798  cdlemk41  36208  mapdheq  37017  hdmap1eq  37091  hdmapval2lem  37123  monotuz  37506  oddcomabszz  37509  nfxnegd  39668  fprodsplit1  39825  dvnmul  40158  sge0sn  40596  hoidmvlelem3  40811