Theorem nfcvd 2892

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

Syntax hints:   → wi 4  Ⅎwnfc 2876

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-nfc 2878

This theorem is referenced by:  nfeld  2903  ralcom2  3351  cbvexeqsetf  3462  sbcralt  3835  sbcrext  3836  csbie2t  3900  sbcco3gw  4388  sbcco3g  4393  csbco3g  4394  dfnfc2  4893  nfdisjw  5086  eusvnfb  5348  eusv2i  5349  dfid3  5536  iota2d  6499  iota2  6500  fmptcof  7102  nfriotadw  7352  riotaeqimp  7370  riota5f  7372  riota5  7373  oprabid  7419  opiota  8038  fmpoco  8074  nfttrcld  9663  axrepndlem1  10545  axrepndlem2  10546  axunnd  10549  axpowndlem2  10551  axpowndlem3  10552  axpowndlem4  10553  axpownd  10554  axregndlem2  10556  axinfndlem1  10558  axinfnd  10559  axacndlem4  10563  axacndlem5  10564  axacnd  10565  nfnegd  11416  prodsn  15928  fprodeq0g  15960  bpolylem  16014  pcmpt  16863  chfacfpmmulfsupp  22750  elmptrab  23714  dvfsumrlim3  25940  itgsubstlem  25955  itgsubst  25956  ifeqeqx  32471  disjunsn  32523  axnulg  35082  bj-elgab  36927  bj-gabima  36928  wl-issetft  37570  unirep  37708  riotasv2d  38950  cdleme31so  40373  cdleme31se  40376  cdleme31sc  40378  cdleme31sde  40379  cdleme31sn2  40383  cdlemeg47rv2  40504  cdlemk41  40914  mapdheq  41722  hdmap1eq  41795  hdmapval2lem  41825  monotuz  42930  oddcomabszz  42933  mnringvald  44202  nfxnegd  45437  fprodsplit1  45591  dvnmul  45941  sge0sn  46377  hoidmvlelem3  46595