Theorem nfcvd 2956

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

Syntax hints:   → wi 4  Ⅎwnfc 2936

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

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786  df-nfc 2938

This theorem is referenced by:  nfeld  2966  nfraldw  3187  ralcom2  3316  nfreuw  3327  nfrmow  3328  vtoclgft  3501  vtoclgftOLD  3502  vtocld  3504  sbcralt  3801  sbcrext  3802  csbied  3864  csbie2t  3866  sbcco3gw  4330  sbcco3g  4335  csbco3g  4336  dfnfc2  4822  nfdisjw  5007  eusvnfb  5259  eusv2i  5260  dfid3  5427  iota2d  6312  iota2  6313  fmptcof  6869  nfriotadw  7101  riotaeqimp  7119  riota5f  7121  riota5  7122  oprabid  7167  opiota  7739  fmpoco  7773  axrepndlem1  10003  axrepndlem2  10004  axunnd  10007  axpowndlem2  10009  axpowndlem3  10010  axpowndlem4  10011  axpownd  10012  axregndlem2  10014  axinfndlem1  10016  axinfnd  10017  axacndlem4  10021  axacndlem5  10022  axacnd  10023  nfnegd  10870  prodsn  15308  fprodeq0g  15340  bpolylem  15394  pcmpt  16218  chfacfpmmulfsupp  21468  elmptrab  22432  dvfsumrlim3  24636  itgsubstlem  24651  itgsubst  24652  ifeqeqx  30309  disjunsn  30357  unirep  35151  riotasv2d  36253  cdleme31so  37675  cdleme31se  37678  cdleme31sc  37680  cdleme31sde  37681  cdleme31sn2  37685  cdlemeg47rv2  37806  cdlemk41  38216  mapdheq  39024  hdmap1eq  39097  hdmapval2lem  39127  monotuz  39882  oddcomabszz  39885  mnringvald  40921  nfxnegd  42078  fprodsplit1  42235  dvnmul  42585  sge0sn  43018  hoidmvlelem3  43236