Theorem nfcvd 2927

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

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

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

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

This theorem is used by:  nfeld  2937  ralcom2  3366  cbvexeqsetf  3469  sbcralt  3823  sbcrext  3824  csbie2t  3889  sbcco3gw  4386  sbcco3g  4391  csbco3g  4392  dfnfc2  4892  eusvnfb  5360  eusv2i  5361  dfid3  5554  iota2d  6548  iota2  6549  fmptcof  7158  nfriotadw  7411  riotaeqimp  7429  riota5f  7431  riota5  7432  oprabid  7478  opiota  8098  fmpoco  8135  nfttrcld  9741  axrepndlem1  10707  axrepndlem2  10708  axunnd  10711  axpowndlem2  10713  axpowndlem3  10714  axpowndlem4  10715  axpownd  10716  axregndlem2  10718  axinfndlem1  10720  axinfnd  10721  axacndlem4  10725  axacndlem5  10726  axacnd  10727  nfnegd  11582  prodsn  16161  fprodeq0g  16193  bpolylem  16246  pcmpt  17102  nfchnd  18817  chfacfpmmulfsupp  23214  elmptrab  24179  dvfsumrlim3  26386  itgsubstlem  26401  itgsubst  26402  ifeqeqx  33213  disjunsn  33263  axsepg2  35921  axnulg  35926  axpowg2  35928  axpowg3  35929  bj-elgab  38043  bj-gabima  38044  wl-issetft  38719  unirep  38853  riotasv2d  40217  cdleme31so  41639  cdleme31se  41642  cdleme31sc  41644  cdleme31sde  41645  cdleme31sn2  41649  cdlemeg47rv2  41770  cdlemk41  42180  mapdheq  42988  hdmap1eq  43061  hdmapval2lem  43091  monotuz  44152  oddcomabszz  44155  mnringvald  45414  nfxnegd  46666  fprodsplit1  46820  dvnmul  47168  sge0sn  47604  hoidmvlelem3  47822