Theorem nfcvd 2893

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

Syntax hints:   → wi 4  Ⅎwnfc 2877

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 2879

This theorem is referenced by:  nfeld  2904  ralcom2  3353  cbvexeqsetf  3465  sbcralt  3837  sbcrext  3838  csbie2t  3902  sbcco3gw  4390  sbcco3g  4395  csbco3g  4396  dfnfc2  4895  nfdisjw  5088  eusvnfb  5350  eusv2i  5351  dfid3  5538  iota2d  6501  iota2  6502  fmptcof  7104  nfriotadw  7354  riotaeqimp  7372  riota5f  7374  riota5  7375  oprabid  7421  opiota  8040  fmpoco  8076  nfttrcld  9669  axrepndlem1  10551  axrepndlem2  10552  axunnd  10555  axpowndlem2  10557  axpowndlem3  10558  axpowndlem4  10559  axpownd  10560  axregndlem2  10562  axinfndlem1  10564  axinfnd  10565  axacndlem4  10569  axacndlem5  10570  axacnd  10571  nfnegd  11422  prodsn  15934  fprodeq0g  15966  bpolylem  16020  pcmpt  16869  chfacfpmmulfsupp  22756  elmptrab  23720  dvfsumrlim3  25946  itgsubstlem  25961  itgsubst  25962  ifeqeqx  32477  disjunsn  32529  axnulg  35088  bj-elgab  36922  bj-gabima  36923  wl-issetft  37565  unirep  37703  riotasv2d  38945  cdleme31so  40368  cdleme31se  40371  cdleme31sc  40373  cdleme31sde  40374  cdleme31sn2  40378  cdlemeg47rv2  40499  cdlemk41  40909  mapdheq  41717  hdmap1eq  41790  hdmapval2lem  41820  monotuz  42923  oddcomabszz  42926  mnringvald  44195  nfxnegd  45430  fprodsplit1  45584  dvnmul  45934  sge0sn  46370  hoidmvlelem3  46588