Theorem nfcvd 2913

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

Syntax hints:   → wi 4  Ⅎwnfc 2899

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

This theorem depends on definitions:  df-bi 197  df-ex 1852  df-nf 1857  df-nfc 2901

This theorem is referenced by:  nfeld  2921  ralcom2  3251  vtoclgft  3403  vtoclgftOLD  3404  vtocld  3406  sbcralt  3658  sbcrext  3659  csbied  3707  csbie2t  3709  sbcco3g  4141  csbco3g  4142  dfnfc2  4590  eusvnfb  4990  eusv2i  4991  dfid3  5158  iota2d  6019  iota2  6020  fmptcof  6539  riotaeqimp  6776  riota5f  6778  riota5  6779  oprabid  6821  opiota  7377  fmpt2co  7410  axrepndlem1  9615  axrepndlem2  9616  axunnd  9619  axpowndlem2  9621  axpowndlem3  9622  axpowndlem4  9623  axpownd  9624  axregndlem2  9626  axinfndlem1  9628  axinfnd  9629  axacndlem4  9633  axacndlem5  9634  axacnd  9635  nfnegd  10477  sumsn  14682  prodsn  14898  fprodeq0g  14930  bpolylem  14984  pcmpt  15802  chfacfpmmulfsupp  20887  elmptrab  21850  dvfsumrlim3  24015  itgsubstlem  24030  itgsubst  24031  ifeqeqx  29693  disjunsn  29739  unirep  33832  riotasv2d  34758  cdleme31so  36181  cdleme31se  36184  cdleme31sc  36186  cdleme31sde  36187  cdleme31sn2  36191  cdlemeg47rv2  36312  cdlemk41  36722  mapdheq  37531  hdmap1eq  37604  hdmapval2lem  37634  monotuz  38025  oddcomabszz  38028  nfxnegd  40178  fprodsplit1  40337  dvnmul  40670  sge0sn  41107  hoidmvlelem3  41325