Theorem nfcvd 2794

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

Syntax hints:   → wi 4  Ⅎwnfc 2780

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

This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750  df-nfc 2782

This theorem is referenced by:  nfeld  2802  ralcom2  3133  vtoclgft  3285  vtoclgftOLD  3286  vtocld  3288  sbcralt  3543  sbcrext  3544  sbcrextOLD  3545  csbied  3593  csbie2t  3595  sbcco3g  4032  csbco3g  4033  dfnfc2  4486  dfnfc2OLD  4487  eusvnfb  4892  eusv2i  4893  dfid3  5054  iota2d  5914  iota2  5915  fmptcof  6437  riotaeqimp  6674  riota5f  6676  riota5  6677  oprabid  6717  opiota  7273  fmpt2co  7305  axrepndlem1  9452  axrepndlem2  9453  axunnd  9456  axpowndlem2  9458  axpowndlem3  9459  axpowndlem4  9460  axpownd  9461  axregndlem2  9463  axinfndlem1  9465  axinfnd  9466  axacndlem4  9470  axacndlem5  9471  axacnd  9472  nfnegd  10314  sumsn  14519  prodsn  14736  fprodeq0g  14769  bpolylem  14823  pcmpt  15643  chfacfpmmulfsupp  20716  elmptrab  21678  dvfsumrlim3  23841  itgsubstlem  23856  itgsubst  23857  ifeqeqx  29487  disjunsn  29533  unirep  33637  riotasv2d  34561  cdleme31so  35984  cdleme31se  35987  cdleme31sc  35989  cdleme31sde  35990  cdleme31sn2  35994  cdlemeg47rv2  36115  cdlemk41  36525  mapdheq  37334  hdmap1eq  37408  hdmapval2lem  37440  monotuz  37823  oddcomabszz  37826  nfxnegd  39981  fprodsplit1  40143  dvnmul  40476  sge0sn  40914  hoidmvlelem3  41132