Theorem nfcvd 2928

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

Syntax hints:   → wi 4  Ⅎwnfc 2912

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

This theorem depends on definitions:  df-bi 210  df-ex 1803  df-nf 1807  df-nfc 2914

This theorem is referenced by:  nfeld  2938  ralcom2  3367  cbvexeqsetf  3472  sbcralt  3828  sbcrext  3829  csbie2t  3893  sbcco3gw  4382  sbcco3g  4387  csbco3g  4388  dfnfc2  4890  eusvnfb  5355  eusv2i  5356  dfid3  5550  iota2d  6513  iota2  6514  fmptcof  7116  nfriotadw  7365  riotaeqimp  7383  riota5f  7385  riota5  7386  oprabid  7432  opiota  8044  fmpoco  8078  nfttrcld  9667  axrepndlem1  10565  axrepndlem2  10566  axunnd  10569  axpowndlem2  10571  axpowndlem3  10572  axpowndlem4  10573  axpownd  10574  axregndlem2  10576  axinfndlem1  10578  axinfnd  10579  axacndlem4  10583  axacndlem5  10584  axacnd  10585  nfnegd  11440  prodsn  16006  fprodeq0g  16038  bpolylem  16092  pcmpt  16942  nfchnd  18657  chfacfpmmulfsupp  22981  elmptrab  23945  dvfsumrlim3  26153  itgsubstlem  26168  itgsubst  26169  ifeqeqx  32798  disjunsn  32849  axsepg2  35448  axnulg  35453  axpowg2  35455  axpowg3  35456  bj-elgab  37436  bj-gabima  37437  wl-issetft  38097  unirep  38225  riotasv2d  39593  cdleme31so  41015  cdleme31se  41018  cdleme31sc  41020  cdleme31sde  41021  cdleme31sn2  41025  cdlemeg47rv2  41146  cdlemk41  41556  mapdheq  42364  hdmap1eq  42437  hdmapval2lem  42467  monotuz  43530  oddcomabszz  43533  mnringvald  44801  nfxnegd  46013  fprodsplit1  46167  dvnmul  46515  sge0sn  46951  hoidmvlelem3  47169