Theorem nfcvd 2900

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 2899	. 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 1797  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786  df-nfc 2886

This theorem is referenced by:  nfeld  2911  ralcom2  3340  cbvexeqsetf  3445  sbcralt  3811  sbcrext  3812  csbie2t  3876  sbcco3gw  4366  sbcco3g  4371  csbco3g  4372  dfnfc2  4873  eusvnfb  5330  eusv2i  5331  dfid3  5522  iota2d  6480  iota2  6481  fmptcof  7077  nfriotadw  7325  riotaeqimp  7343  riota5f  7345  riota5  7346  oprabid  7392  opiota  8005  fmpoco  8038  nfttrcld  9622  axrepndlem1  10506  axrepndlem2  10507  axunnd  10510  axpowndlem2  10512  axpowndlem3  10513  axpowndlem4  10514  axpownd  10515  axregndlem2  10517  axinfndlem1  10519  axinfnd  10520  axacndlem4  10524  axacndlem5  10525  axacnd  10526  nfnegd  11379  prodsn  15918  fprodeq0g  15950  bpolylem  16004  pcmpt  16854  nfchnd  18568  chfacfpmmulfsupp  22838  elmptrab  23802  dvfsumrlim3  26010  itgsubstlem  26025  itgsubst  26026  ifeqeqx  32627  disjunsn  32679  axnulg  35267  bj-elgab  37262  bj-gabima  37263  wl-issetft  37921  unirep  38049  riotasv2d  39417  cdleme31so  40839  cdleme31se  40842  cdleme31sc  40844  cdleme31sde  40845  cdleme31sn2  40849  cdlemeg47rv2  40970  cdlemk41  41380  mapdheq  42188  hdmap1eq  42261  hdmapval2lem  42291  monotuz  43387  oddcomabszz  43390  mnringvald  44658  nfxnegd  45887  fprodsplit1  46041  dvnmul  46389  sge0sn  46825  hoidmvlelem3  47043