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  3349  cbvexeqsetf  3457  sbcralt  3824  sbcrext  3825  csbie2t  3889  sbcco3gw  4379  sbcco3g  4384  csbco3g  4385  dfnfc2  4887  nfdisjw  5079  eusvnfb  5340  eusv2i  5341  dfid3  5530  iota2d  6488  iota2  6489  fmptcof  7085  nfriotadw  7333  riotaeqimp  7351  riota5f  7353  riota5  7354  oprabid  7400  opiota  8013  fmpoco  8047  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  11387  prodsn  15897  fprodeq0g  15929  bpolylem  15983  pcmpt  16832  nfchnd  18546  chfacfpmmulfsupp  22819  elmptrab  23783  dvfsumrlim3  26008  itgsubstlem  26023  itgsubst  26024  ifeqeqx  32628  disjunsn  32680  axnulg  35283  bj-elgab  37181  bj-gabima  37182  wl-issetft  37831  unirep  37959  riotasv2d  39327  cdleme31so  40749  cdleme31se  40752  cdleme31sc  40754  cdleme31sde  40755  cdleme31sn2  40759  cdlemeg47rv2  40880  cdlemk41  41290  mapdheq  42098  hdmap1eq  42171  hdmapval2lem  42201  monotuz  43292  oddcomabszz  43295  mnringvald  44563  nfxnegd  45793  fprodsplit1  45947  dvnmul  46295  sge0sn  46731  hoidmvlelem3  46949