Theorem nfcvd 2909

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

Syntax hints:   → wi 4  Ⅎwnfc 2893

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

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782  df-nfc 2895

This theorem is referenced by:  nfeld  2920  nfraldwOLD  3328  ralcom2  3385  nfreuwOLD  3433  nfrmowOLD  3434  cbvexeqsetf  3503  sbcralt  3894  sbcrext  3895  csbiedOLD  3960  csbie2t  3962  sbcco3gw  4448  sbcco3g  4453  csbco3g  4454  dfnfc2  4953  nfdisjw  5145  eusvnfb  5411  eusv2i  5412  dfid3  5596  iota2d  6561  iota2  6562  fmptcof  7164  nfriotadw  7412  riotaeqimp  7431  riota5f  7433  riota5  7434  oprabid  7480  opiota  8100  fmpoco  8136  nfttrcld  9779  axrepndlem1  10661  axrepndlem2  10662  axunnd  10665  axpowndlem2  10667  axpowndlem3  10668  axpowndlem4  10669  axpownd  10670  axregndlem2  10672  axinfndlem1  10674  axinfnd  10675  axacndlem4  10679  axacndlem5  10680  axacnd  10681  nfnegd  11531  prodsn  16010  fprodeq0g  16042  bpolylem  16096  pcmpt  16939  chfacfpmmulfsupp  22890  elmptrab  23856  dvfsumrlim3  26094  itgsubstlem  26109  itgsubst  26110  ifeqeqx  32565  disjunsn  32616  axnulg  35068  bj-elgab  36905  bj-gabima  36906  wl-issetft  37536  unirep  37674  riotasv2d  38913  cdleme31so  40336  cdleme31se  40339  cdleme31sc  40341  cdleme31sde  40342  cdleme31sn2  40346  cdlemeg47rv2  40467  cdlemk41  40877  mapdheq  41685  hdmap1eq  41758  hdmapval2lem  41788  monotuz  42898  oddcomabszz  42901  mnringvald  44177  nfxnegd  45356  fprodsplit1  45514  dvnmul  45864  sge0sn  46300  hoidmvlelem3  46518