Theorem nfcvd 2893

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

Syntax hints:   → wi 4  Ⅎwnfc 2877

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-nfc 2879

This theorem is referenced by:  nfeld  2904  ralcom2  3353  cbvexeqsetf  3465  sbcralt  3838  sbcrext  3839  csbie2t  3903  sbcco3gw  4391  sbcco3g  4396  csbco3g  4397  dfnfc2  4896  nfdisjw  5089  eusvnfb  5351  eusv2i  5352  dfid3  5539  iota2d  6502  iota2  6503  fmptcof  7105  nfriotadw  7355  riotaeqimp  7373  riota5f  7375  riota5  7376  oprabid  7422  opiota  8041  fmpoco  8077  nfttrcld  9670  axrepndlem1  10552  axrepndlem2  10553  axunnd  10556  axpowndlem2  10558  axpowndlem3  10559  axpowndlem4  10560  axpownd  10561  axregndlem2  10563  axinfndlem1  10565  axinfnd  10566  axacndlem4  10570  axacndlem5  10571  axacnd  10572  nfnegd  11423  prodsn  15935  fprodeq0g  15967  bpolylem  16021  pcmpt  16870  chfacfpmmulfsupp  22757  elmptrab  23721  dvfsumrlim3  25947  itgsubstlem  25962  itgsubst  25963  ifeqeqx  32478  disjunsn  32530  axnulg  35089  bj-elgab  36934  bj-gabima  36935  wl-issetft  37577  unirep  37715  riotasv2d  38957  cdleme31so  40380  cdleme31se  40383  cdleme31sc  40385  cdleme31sde  40386  cdleme31sn2  40390  cdlemeg47rv2  40511  cdlemk41  40921  mapdheq  41729  hdmap1eq  41802  hdmapval2lem  41832  monotuz  42937  oddcomabszz  42940  mnringvald  44209  nfxnegd  45444  fprodsplit1  45598  dvnmul  45948  sge0sn  46384  hoidmvlelem3  46602