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 ⊢ (𝜑 → Ⅎ𝑥𝐴)

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

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

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

This theorem is used by:  nfeld  2934  ralcom2  3363  cbvexeqsetf  3466  sbcralt  3819  sbcrext  3820  csbie2t  3885  sbcco3gw  4383  sbcco3g  4388  csbco3g  4389  dfnfc2  4889  eusvnfb  5355  eusv2i  5356  dfid3  5549  iota2d  6519  iota2  6520  fmptcof  7123  nfriotadw  7377  riotaeqimp  7395  riota5f  7397  riota5  7398  oprabid  7444  opiota  8059  fmpoco  8095  nfttrcld  9695  axrepndlem1  10658  axrepndlem2  10659  axunnd  10662  axpowndlem2  10664  axpowndlem3  10665  axpowndlem4  10666  axpownd  10667  axregndlem2  10669  axinfndlem1  10671  axinfnd  10672  axacndlem4  10676  axacndlem5  10677  axacnd  10678  nfnegd  11533  prodsn  16109  fprodeq0g  16141  bpolylem  16194  pcmpt  17050  nfchnd  18765  chfacfpmmulfsupp  23161  elmptrab  24126  dvfsumrlim3  26333  itgsubstlem  26348  itgsubst  26349  ifeqeqx  33120  disjunsn  33170  axsepg2  35781  axnulg  35786  axpowg2  35788  axpowg3  35789  bj-elgab  37822  bj-gabima  37823  wl-issetft  38482  unirep  38616  riotasv2d  39982  cdleme31so  41404  cdleme31se  41407  cdleme31sc  41409  cdleme31sde  41410  cdleme31sn2  41414  cdlemeg47rv2  41535  cdlemk41  41945  mapdheq  42753  hdmap1eq  42826  hdmapval2lem  42856  monotuz  43901  oddcomabszz  43904  mnringvald  45170  nfxnegd  46395  fprodsplit1  46549  dvnmul  46897  sge0sn  47333  hoidmvlelem3  47551