Theorem nfcvd 2923

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

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

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

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816  df-nfc 2909

This theorem is used by:  nfeld  2933  ralcom2  3362  cbvexeqsetf  3465  sbcralt  3818  sbcrext  3819  csbie2t  3884  sbcco3gw  4382  sbcco3g  4387  csbco3g  4388  dfnfc2  4888  eusvnfb  5354  eusv2i  5355  dfid3  5548  iota2d  6526  iota2  6527  fmptcof  7131  nfriotadw  7385  riotaeqimp  7403  riota5f  7405  riota5  7406  oprabid  7452  opiota  8070  fmpoco  8107  nfttrcld  9714  axrepndlem1  10680  axrepndlem2  10681  axunnd  10684  axpowndlem2  10686  axpowndlem3  10687  axpowndlem4  10688  axpownd  10689  axregndlem2  10691  axinfndlem1  10693  axinfnd  10694  axacndlem4  10698  axacndlem5  10699  axacnd  10700  nfnegd  11555  prodsn  16134  fprodeq0g  16166  bpolylem  16219  pcmpt  17075  nfchnd  18790  chfacfpmmulfsupp  23186  elmptrab  24151  dvfsumrlim3  26358  itgsubstlem  26373  itgsubst  26374  ifeqeqx  33185  disjunsn  33235  axsepg2  35864  axnulg  35869  axpowg2  35871  axpowg3  35872  bj-elgab  37944  bj-gabima  37945  wl-issetft  38607  unirep  38741  riotasv2d  40107  cdleme31so  41529  cdleme31se  41532  cdleme31sc  41534  cdleme31sde  41535  cdleme31sn2  41539  cdlemeg47rv2  41660  cdlemk41  42070  mapdheq  42878  hdmap1eq  42951  hdmapval2lem  42981  monotuz  44041  oddcomabszz  44044  mnringvald  45304  nfxnegd  46544  fprodsplit1  46698  dvnmul  47046  sge0sn  47482  hoidmvlelem3  47700