Theorem nfcvd 2899

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

Syntax hints:   → wi 4  Ⅎwnfc 2883

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 2885

This theorem is referenced by:  nfeld  2910  ralcom2  3356  nfreuwOLD  3405  nfrmowOLD  3406  cbvexeqsetf  3474  sbcralt  3847  sbcrext  3848  csbie2t  3912  sbcco3gw  4400  sbcco3g  4405  csbco3g  4406  dfnfc2  4905  nfdisjw  5098  eusvnfb  5363  eusv2i  5364  dfid3  5551  iota2d  6519  iota2  6520  fmptcof  7120  nfriotadw  7370  riotaeqimp  7388  riota5f  7390  riota5  7391  oprabid  7437  opiota  8058  fmpoco  8094  nfttrcld  9724  axrepndlem1  10606  axrepndlem2  10607  axunnd  10610  axpowndlem2  10612  axpowndlem3  10613  axpowndlem4  10614  axpownd  10615  axregndlem2  10617  axinfndlem1  10619  axinfnd  10620  axacndlem4  10624  axacndlem5  10625  axacnd  10626  nfnegd  11477  prodsn  15978  fprodeq0g  16010  bpolylem  16064  pcmpt  16912  chfacfpmmulfsupp  22801  elmptrab  23765  dvfsumrlim3  25992  itgsubstlem  26007  itgsubst  26008  ifeqeqx  32523  disjunsn  32575  axnulg  35123  bj-elgab  36957  bj-gabima  36958  wl-issetft  37600  unirep  37738  riotasv2d  38975  cdleme31so  40398  cdleme31se  40401  cdleme31sc  40403  cdleme31sde  40404  cdleme31sn2  40408  cdlemeg47rv2  40529  cdlemk41  40939  mapdheq  41747  hdmap1eq  41820  hdmapval2lem  41850  monotuz  42965  oddcomabszz  42968  mnringvald  44237  nfxnegd  45468  fprodsplit1  45622  dvnmul  45972  sge0sn  46408  hoidmvlelem3  46626