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

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

This theorem is referenced by:  nfeld  2910  ralcom2  3339  cbvexeqsetf  3444  sbcralt  3810  sbcrext  3811  csbie2t  3875  sbcco3gw  4365  sbcco3g  4370  csbco3g  4371  dfnfc2  4872  eusvnfb  5335  eusv2i  5336  dfid3  5529  iota2d  6486  iota2  6487  fmptcof  7083  nfriotadw  7332  riotaeqimp  7350  riota5f  7352  riota5  7353  oprabid  7399  opiota  8012  fmpoco  8045  nfttrcld  9631  axrepndlem1  10515  axrepndlem2  10516  axunnd  10519  axpowndlem2  10521  axpowndlem3  10522  axpowndlem4  10523  axpownd  10524  axregndlem2  10526  axinfndlem1  10528  axinfnd  10529  axacndlem4  10533  axacndlem5  10534  axacnd  10535  nfnegd  11388  prodsn  15927  fprodeq0g  15959  bpolylem  16013  pcmpt  16863  nfchnd  18577  chfacfpmmulfsupp  22828  elmptrab  23792  dvfsumrlim3  26000  itgsubstlem  26015  itgsubst  26016  ifeqeqx  32612  disjunsn  32664  axnulg  35251  bj-elgab  37246  bj-gabima  37247  wl-issetft  37907  unirep  38035  riotasv2d  39403  cdleme31so  40825  cdleme31se  40828  cdleme31sc  40830  cdleme31sde  40831  cdleme31sn2  40835  cdlemeg47rv2  40956  cdlemk41  41366  mapdheq  42174  hdmap1eq  42247  hdmapval2lem  42277  monotuz  43369  oddcomabszz  43372  mnringvald  44640  nfxnegd  45869  fprodsplit1  46023  dvnmul  46371  sge0sn  46807  hoidmvlelem3  47025