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  3342  cbvexeqsetf  3453  sbcralt  3826  sbcrext  3827  csbie2t  3891  sbcco3gw  4378  sbcco3g  4383  csbco3g  4384  dfnfc2  4883  nfdisjw  5074  eusvnfb  5335  eusv2i  5336  dfid3  5521  iota2d  6474  iota2  6475  fmptcof  7068  nfriotadw  7318  riotaeqimp  7336  riota5f  7338  riota5  7339  oprabid  7385  opiota  8001  fmpoco  8035  nfttrcld  9625  axrepndlem1  10505  axrepndlem2  10506  axunnd  10509  axpowndlem2  10511  axpowndlem3  10512  axpowndlem4  10513  axpownd  10514  axregndlem2  10516  axinfndlem1  10518  axinfnd  10519  axacndlem4  10523  axacndlem5  10524  axacnd  10525  nfnegd  11376  prodsn  15887  fprodeq0g  15919  bpolylem  15973  pcmpt  16822  chfacfpmmulfsupp  22766  elmptrab  23730  dvfsumrlim3  25956  itgsubstlem  25971  itgsubst  25972  ifeqeqx  32504  disjunsn  32556  axnulg  35058  bj-elgab  36912  bj-gabima  36913  wl-issetft  37555  unirep  37693  riotasv2d  38935  cdleme31so  40358  cdleme31se  40361  cdleme31sc  40363  cdleme31sde  40364  cdleme31sn2  40368  cdlemeg47rv2  40489  cdlemk41  40899  mapdheq  41707  hdmap1eq  41780  hdmapval2lem  41810  monotuz  42914  oddcomabszz  42917  mnringvald  44186  nfxnegd  45421  fprodsplit1  45575  dvnmul  45925  sge0sn  46361  hoidmvlelem3  46579