Theorem nfcvd 2752

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

Syntax hints:   → wi 4  Ⅎwnfc 2738

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

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701  df-nfc 2740

This theorem is referenced by:  nfeld  2759  ralcom2  3083  vtoclgft  3227  vtoclgftOLD  3228  vtocld  3230  sbcralt  3477  sbcrext  3478  sbcrextOLD  3479  csbied  3526  csbie2t  3528  sbcco3g  3951  csbco3g  3952  dfnfc2  4390  dfnfc2OLD  4391  eusvnfb  4788  eusv2i  4789  dfid3  4954  nfiotad  5771  iota2d  5793  iota2  5794  fmptcof  6304  riota5f  6535  riota5  6536  oprabid  6576  opiota  7118  fmpt2co  7147  axrepndlem1  9293  axrepndlem2  9294  axunnd  9297  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axpownd  9302  axregndlem2  9304  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  nfnegd  10155  sumsn  14319  prodsn  14531  fprodeq0g  14564  bpolylem  14618  pcmpt  15434  chfacfpmmulfsupp  20487  elmptrab  21440  dvfsumrlim3  23600  itgsubstlem  23615  itgsubst  23616  ifeqeqx  28745  disjunsn  28789  unirep  32677  riotasv2d  33261  cdleme31so  34685  cdleme31se  34688  cdleme31sc  34690  cdleme31sde  34691  cdleme31sn2  34695  cdlemeg47rv2  34816  cdlemk41  35226  mapdheq  36035  hdmap1eq  36109  hdmapval2lem  36141  monotuz  36524  oddcomabszz  36527  fprodsplit1  38660  dvnmul  38833  sge0sn  39272  hoidmvlelem3  39487  riotaeqimp  40338