Theorem nfcvd 2764

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

Syntax hints:   → wi 4  Ⅎwnfc 2750

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

This theorem depends on definitions:  df-bi 197  df-ex 1704  df-nf 1709  df-nfc 2752

This theorem is referenced by:  nfeld  2772  ralcom2  3102  vtoclgft  3252  vtoclgftOLD  3253  vtocld  3255  sbcralt  3508  sbcrext  3509  sbcrextOLD  3510  csbied  3558  csbie2t  3560  sbcco3g  3997  csbco3g  3998  dfnfc2  4452  dfnfc2OLD  4453  eusvnfb  4860  eusv2i  4861  dfid3  5023  iota2d  5874  iota2  5875  fmptcof  6395  riotaeqimp  6631  riota5f  6633  riota5  6634  oprabid  6674  opiota  7226  fmpt2co  7257  axrepndlem1  9411  axrepndlem2  9412  axunnd  9415  axpowndlem2  9417  axpowndlem3  9418  axpowndlem4  9419  axpownd  9420  axregndlem2  9422  axinfndlem1  9424  axinfnd  9425  axacndlem4  9429  axacndlem5  9430  axacnd  9431  nfnegd  10273  sumsn  14469  prodsn  14686  fprodeq0g  14719  bpolylem  14773  pcmpt  15590  chfacfpmmulfsupp  20662  elmptrab  21624  dvfsumrlim3  23790  itgsubstlem  23805  itgsubst  23806  ifeqeqx  29345  disjunsn  29391  unirep  33487  riotasv2d  34069  cdleme31so  35493  cdleme31se  35496  cdleme31sc  35498  cdleme31sde  35499  cdleme31sn2  35503  cdlemeg47rv2  35624  cdlemk41  36034  mapdheq  36843  hdmap1eq  36917  hdmapval2lem  36949  monotuz  37332  oddcomabszz  37335  nfxnegd  39487  fprodsplit1  39631  dvnmul  39927  sge0sn  40365  hoidmvlelem3  40580