Theorem nfcvd 2899

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

Syntax hints:   → wi 4  Ⅎwnfc 2883

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

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785  df-nfc 2885

This theorem is referenced by:  nfeld  2910  ralcom2  3347  cbvexeqsetf  3455  sbcralt  3822  sbcrext  3823  csbie2t  3887  sbcco3gw  4377  sbcco3g  4382  csbco3g  4383  dfnfc2  4885  nfdisjw  5077  eusvnfb  5338  eusv2i  5339  dfid3  5522  iota2d  6480  iota2  6481  fmptcof  7075  nfriotadw  7323  riotaeqimp  7341  riota5f  7343  riota5  7344  oprabid  7390  opiota  8003  fmpoco  8037  nfttrcld  9619  axrepndlem1  10503  axrepndlem2  10504  axunnd  10507  axpowndlem2  10509  axpowndlem3  10510  axpowndlem4  10511  axpownd  10512  axregndlem2  10514  axinfndlem1  10516  axinfnd  10517  axacndlem4  10521  axacndlem5  10522  axacnd  10523  nfnegd  11375  prodsn  15885  fprodeq0g  15917  bpolylem  15971  pcmpt  16820  nfchnd  18534  chfacfpmmulfsupp  22807  elmptrab  23771  dvfsumrlim3  25996  itgsubstlem  26011  itgsubst  26012  ifeqeqx  32617  disjunsn  32669  axnulg  35264  bj-elgab  37140  bj-gabima  37141  wl-issetft  37783  unirep  37911  riotasv2d  39213  cdleme31so  40635  cdleme31se  40638  cdleme31sc  40640  cdleme31sde  40641  cdleme31sn2  40645  cdlemeg47rv2  40766  cdlemk41  41176  mapdheq  41984  hdmap1eq  42057  hdmapval2lem  42087  monotuz  43179  oddcomabszz  43182  mnringvald  44450  nfxnegd  45681  fprodsplit1  45835  dvnmul  46183  sge0sn  46619  hoidmvlelem3  46837