Theorem nfcvd 2929

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

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

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 2915

This theorem is used by:  nfeld  2939  ralcom2  3369  cbvexeqsetf  3473  sbcralt  3828  sbcrext  3829  csbie2t  3894  sbcco3gw  4393  sbcco3g  4398  csbco3g  4399  dfnfc2  4899  eusvnfb  5369  eusv2i  5370  dfid3  5564  iota2d  6531  iota2  6532  fmptcof  7133  nfriotadw  7388  riotaeqimp  7406  riota5f  7408  riota5  7409  oprabid  7455  opiota  8065  fmpoco  8099  nfttrcld  9689  axrepndlem1  10595  axrepndlem2  10596  axunnd  10599  axpowndlem2  10601  axpowndlem3  10602  axpowndlem4  10603  axpownd  10604  axregndlem2  10606  axinfndlem1  10608  axinfnd  10609  axacndlem4  10613  axacndlem5  10614  axacnd  10615  nfnegd  11470  prodsn  16042  fprodeq0g  16074  bpolylem  16127  pcmpt  16977  nfchnd  18692  chfacfpmmulfsupp  23057  elmptrab  24021  dvfsumrlim3  26229  itgsubstlem  26244  itgsubst  26245  ifeqeqx  32925  disjunsn  32976  axsepg2  35577  axnulg  35582  axpowg2  35584  axpowg3  35585  bj-elgab  37616  bj-gabima  37617  wl-issetft  38278  unirep  38406  riotasv2d  39772  cdleme31so  41194  cdleme31se  41197  cdleme31sc  41199  cdleme31sde  41200  cdleme31sn2  41204  cdlemeg47rv2  41325  cdlemk41  41735  mapdheq  42543  hdmap1eq  42616  hdmapval2lem  42646  monotuz  43709  oddcomabszz  43712  mnringvald  44978  nfxnegd  46196  fprodsplit1  46350  dvnmul  46698  sge0sn  47134  hoidmvlelem3  47352