Theorem nfcvd 2896

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

Syntax hints:   → wi 4  Ⅎwnfc 2875

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

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778  df-nfc 2877

This theorem is referenced by:  nfeld  2906  nfraldwOLD  3310  ralcom2  3365  nfreuwOLD  3414  nfrmowOLD  3415  issetft  3480  vtocldOLD  3541  sbcralt  3858  sbcrext  3859  csbiedOLD  3924  csbie2t  3926  sbcco3gw  4414  sbcco3g  4419  csbco3g  4420  dfnfc2  4923  nfdisjw  5115  eusvnfb  5381  eusv2i  5382  dfid3  5567  iota2d  6521  iota2  6522  fmptcof  7120  nfriotadw  7365  riotaeqimp  7384  riota5f  7386  riota5  7387  oprabid  7433  opiota  8038  fmpoco  8075  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  11452  prodsn  15903  fprodeq0g  15935  bpolylem  15989  pcmpt  16824  chfacfpmmulfsupp  22687  elmptrab  23653  dvfsumrlim3  25890  itgsubstlem  25905  itgsubst  25906  ifeqeqx  32243  disjunsn  32294  bj-elgab  36309  bj-gabima  36310  wl-issetft  36934  unirep  37072  riotasv2d  38317  cdleme31so  39740  cdleme31se  39743  cdleme31sc  39745  cdleme31sde  39746  cdleme31sn2  39750  cdlemeg47rv2  39871  cdlemk41  40281  mapdheq  41089  hdmap1eq  41162  hdmapval2lem  41192  monotuz  42169  oddcomabszz  42172  mnringvald  43456  nfxnegd  44636  fprodsplit1  44794  dvnmul  45144  sge0sn  45580  hoidmvlelem3  45798