Theorem nfcvd 2924

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

Syntax hints:   → wi 4  Ⅎwnfc 2908

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

This theorem depends on definitions:  df-bi 210  df-ex 1808  df-nf 1812  df-nfc 2910

This theorem is referenced by:  nfeld  2934  ralcom2  3364  cbvexeqsetf  3468  sbcralt  3824  sbcrext  3825  csbie2t  3890  sbcco3gw  4389  sbcco3g  4394  csbco3g  4395  dfnfc2  4893  eusvnfb  5364  eusv2i  5365  dfid3  5559  iota2d  6524  iota2  6525  fmptcof  7126  nfriotadw  7375  riotaeqimp  7393  riota5f  7395  riota5  7396  oprabid  7442  opiota  8055  fmpoco  8089  nfttrcld  9678  axrepndlem1  10576  axrepndlem2  10577  axunnd  10580  axpowndlem2  10582  axpowndlem3  10583  axpowndlem4  10584  axpownd  10585  axregndlem2  10587  axinfndlem1  10589  axinfnd  10590  axacndlem4  10594  axacndlem5  10595  axacnd  10596  nfnegd  11451  prodsn  16015  fprodeq0g  16047  bpolylem  16101  pcmpt  16951  nfchnd  18666  chfacfpmmulfsupp  22999  elmptrab  23963  dvfsumrlim3  26171  itgsubstlem  26186  itgsubst  26187  ifeqeqx  32854  disjunsn  32905  axsepg2  35507  axnulg  35512  axpowg2  35514  axpowg3  35515  bj-elgab  37519  bj-gabima  37520  wl-issetft  38181  unirep  38309  riotasv2d  39677  cdleme31so  41099  cdleme31se  41102  cdleme31sc  41104  cdleme31sde  41105  cdleme31sn2  41109  cdlemeg47rv2  41230  cdlemk41  41640  mapdheq  42448  hdmap1eq  42521  hdmapval2lem  42551  monotuz  43616  oddcomabszz  43619  mnringvald  44885  nfxnegd  46103  fprodsplit1  46257  dvnmul  46605  sge0sn  47041  hoidmvlelem3  47259