Theorem nfcvd 2903

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

Syntax hints:   → wi 4  Ⅎwnfc 2887

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

This theorem depends on definitions:  df-bi 207  df-ex 1776  df-nf 1780  df-nfc 2889

This theorem is referenced by:  nfeld  2914  ralcom2  3374  nfreuwOLD  3422  nfrmowOLD  3423  cbvexeqsetf  3492  sbcralt  3880  sbcrext  3881  csbiedOLD  3946  csbie2t  3948  sbcco3gw  4430  sbcco3g  4435  csbco3g  4436  dfnfc2  4933  nfdisjw  5126  eusvnfb  5398  eusv2i  5399  dfid3  5585  iota2d  6550  iota2  6551  fmptcof  7149  nfriotadw  7395  riotaeqimp  7413  riota5f  7415  riota5  7416  oprabid  7462  opiota  8082  fmpoco  8118  nfttrcld  9747  axrepndlem1  10629  axrepndlem2  10630  axunnd  10633  axpowndlem2  10635  axpowndlem3  10636  axpowndlem4  10637  axpownd  10638  axregndlem2  10640  axinfndlem1  10642  axinfnd  10643  axacndlem4  10647  axacndlem5  10648  axacnd  10649  nfnegd  11500  prodsn  15994  fprodeq0g  16026  bpolylem  16080  pcmpt  16925  chfacfpmmulfsupp  22884  elmptrab  23850  dvfsumrlim3  26088  itgsubstlem  26103  itgsubst  26104  ifeqeqx  32562  disjunsn  32613  axnulg  35084  bj-elgab  36921  bj-gabima  36922  wl-issetft  37562  unirep  37700  riotasv2d  38938  cdleme31so  40361  cdleme31se  40364  cdleme31sc  40366  cdleme31sde  40367  cdleme31sn2  40371  cdlemeg47rv2  40492  cdlemk41  40902  mapdheq  41710  hdmap1eq  41783  hdmapval2lem  41813  monotuz  42929  oddcomabszz  42932  mnringvald  44203  nfxnegd  45390  fprodsplit1  45548  dvnmul  45898  sge0sn  46334  hoidmvlelem3  46552