Theorem nfcvd 2926

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

Syntax hints:   → wi 4  Ⅎwnfc 2910

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

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814  df-nfc 2912

This theorem is referenced by:  nfeld  2936  ralcom2  3366  cbvexeqsetf  3470  sbcralt  3826  sbcrext  3827  csbie2t  3892  sbcco3gw  4391  sbcco3g  4396  csbco3g  4397  dfnfc2  4895  eusvnfb  5366  eusv2i  5367  dfid3  5561  iota2d  6526  iota2  6527  fmptcof  7128  nfriotadw  7377  riotaeqimp  7395  riota5f  7397  riota5  7398  oprabid  7444  opiota  8057  fmpoco  8091  nfttrcld  9680  axrepndlem1  10578  axrepndlem2  10579  axunnd  10582  axpowndlem2  10584  axpowndlem3  10585  axpowndlem4  10586  axpownd  10587  axregndlem2  10589  axinfndlem1  10591  axinfnd  10592  axacndlem4  10596  axacndlem5  10597  axacnd  10598  nfnegd  11453  prodsn  16018  fprodeq0g  16050  bpolylem  16103  pcmpt  16953  nfchnd  18668  chfacfpmmulfsupp  23001  elmptrab  23965  dvfsumrlim3  26173  itgsubstlem  26188  itgsubst  26189  ifeqeqx  32866  disjunsn  32917  axsepg2  35531  axnulg  35536  axpowg2  35538  axpowg3  35539  bj-elgab  37553  bj-gabima  37554  wl-issetft  38215  unirep  38343  riotasv2d  39709  cdleme31so  41131  cdleme31se  41134  cdleme31sc  41136  cdleme31sde  41137  cdleme31sn2  41141  cdlemeg47rv2  41262  cdlemk41  41672  mapdheq  42480  hdmap1eq  42553  hdmapval2lem  42583  monotuz  43648  oddcomabszz  43651  mnringvald  44917  nfxnegd  46135  fprodsplit1  46289  dvnmul  46637  sge0sn  47073  hoidmvlelem3  47291