Theorem nfcvd 2925

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnfc 2909

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817  df-nfc 2911

This theorem is used by:  nfeld  2935  ralcom2  3364  cbvexeqsetf  3468  sbcralt  3822  sbcrext  3823  csbie2t  3888  sbcco3gw  4386  sbcco3g  4391  csbco3g  4392  dfnfc2  4892  eusvnfb  5362  eusv2i  5363  dfid3  5557  iota2d  6525  iota2  6526  fmptcof  7128  nfriotadw  7382  riotaeqimp  7400  riota5f  7402  riota5  7403  oprabid  7449  opiota  8060  fmpoco  8096  nfttrcld  9693  axrepndlem1  10605  axrepndlem2  10606  axunnd  10609  axpowndlem2  10611  axpowndlem3  10612  axpowndlem4  10613  axpownd  10614  axregndlem2  10616  axinfndlem1  10618  axinfnd  10619  axacndlem4  10623  axacndlem5  10624  axacnd  10625  nfnegd  11480  prodsn  16055  fprodeq0g  16087  bpolylem  16140  pcmpt  16990  nfchnd  18705  chfacfpmmulfsupp  23094  elmptrab  24059  dvfsumrlim3  26267  itgsubstlem  26282  itgsubst  26283  ifeqeqx  33025  disjunsn  33075  axsepg2  35674  axnulg  35679  axpowg2  35681  axpowg3  35682  bj-elgab  37691  bj-gabima  37692  wl-issetft  38353  unirep  38472  riotasv2d  39838  cdleme31so  41260  cdleme31se  41263  cdleme31sc  41265  cdleme31sde  41266  cdleme31sn2  41270  cdlemeg47rv2  41391  cdlemk41  41801  mapdheq  42609  hdmap1eq  42682  hdmapval2lem  42712  monotuz  43790  oddcomabszz  43793  mnringvald  45059  nfxnegd  46277  fprodsplit1  46431  dvnmul  46779  sge0sn  47215  hoidmvlelem3  47433