Theorem nfcvd 2907

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

Syntax hints:   → wi 4  Ⅎwnfc 2886

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

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788  df-nfc 2888

This theorem is referenced by:  nfeld  2917  nfraldwOLD  3147  ralcom2  3288  nfreuw  3300  nfrmow  3301  vtoclgft  3482  vtocldOLD  3485  sbcralt  3801  sbcrext  3802  csbiedOLD  3867  csbie2t  3869  sbcco3gw  4353  sbcco3g  4358  csbco3g  4359  dfnfc2  4860  nfdisjw  5047  eusvnfb  5311  eusv2i  5312  dfid3  5483  iota2d  6406  iota2  6407  fmptcof  6984  nfriotadw  7220  riotaeqimp  7239  riota5f  7241  riota5  7242  oprabid  7287  opiota  7872  fmpoco  7906  axrepndlem1  10279  axrepndlem2  10280  axunnd  10283  axpowndlem2  10285  axpowndlem3  10286  axpowndlem4  10287  axpownd  10288  axregndlem2  10290  axinfndlem1  10292  axinfnd  10293  axacndlem4  10297  axacndlem5  10298  axacnd  10299  nfnegd  11146  prodsn  15600  fprodeq0g  15632  bpolylem  15686  pcmpt  16521  chfacfpmmulfsupp  21920  elmptrab  22886  dvfsumrlim3  25102  itgsubstlem  25117  itgsubst  25118  ifeqeqx  30786  disjunsn  30834  nfttrcld  33696  bj-elgab  35054  bj-gabima  35055  unirep  35798  riotasv2d  36898  cdleme31so  38320  cdleme31se  38323  cdleme31sc  38325  cdleme31sde  38326  cdleme31sn2  38330  cdlemeg47rv2  38451  cdlemk41  38861  mapdheq  39669  hdmap1eq  39742  hdmapval2lem  39772  monotuz  40679  oddcomabszz  40682  mnringvald  41715  nfxnegd  42871  fprodsplit1  43024  dvnmul  43374  sge0sn  43807  hoidmvlelem3  44025