Theorem nfcvd 2906

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

Syntax hints:   → wi 4  Ⅎwnfc 2890

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 2892

This theorem is referenced by:  nfeld  2917  ralcom2  3377  nfreuwOLD  3426  nfrmowOLD  3427  cbvexeqsetf  3495  sbcralt  3872  sbcrext  3873  csbie2t  3937  sbcco3gw  4425  sbcco3g  4430  csbco3g  4431  dfnfc2  4929  nfdisjw  5122  eusvnfb  5393  eusv2i  5394  dfid3  5581  iota2d  6549  iota2  6550  fmptcof  7150  nfriotadw  7396  riotaeqimp  7414  riota5f  7416  riota5  7417  oprabid  7463  opiota  8084  fmpoco  8120  nfttrcld  9750  axrepndlem1  10632  axrepndlem2  10633  axunnd  10636  axpowndlem2  10638  axpowndlem3  10639  axpowndlem4  10640  axpownd  10641  axregndlem2  10643  axinfndlem1  10645  axinfnd  10646  axacndlem4  10650  axacndlem5  10651  axacnd  10652  nfnegd  11503  prodsn  15998  fprodeq0g  16030  bpolylem  16084  pcmpt  16930  chfacfpmmulfsupp  22869  elmptrab  23835  dvfsumrlim3  26074  itgsubstlem  26089  itgsubst  26090  ifeqeqx  32555  disjunsn  32607  axnulg  35106  bj-elgab  36940  bj-gabima  36941  wl-issetft  37583  unirep  37721  riotasv2d  38958  cdleme31so  40381  cdleme31se  40384  cdleme31sc  40386  cdleme31sde  40387  cdleme31sn2  40391  cdlemeg47rv2  40512  cdlemk41  40922  mapdheq  41730  hdmap1eq  41803  hdmapval2lem  41833  monotuz  42953  oddcomabszz  42956  mnringvald  44227  nfxnegd  45452  fprodsplit1  45608  dvnmul  45958  sge0sn  46394  hoidmvlelem3  46612