Theorem nfcvd 2924

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

Syntax hints:   → wi 4  Ⅎwnfc 2908

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

This theorem depends on definitions:  df-bi 209  df-ex 1799  df-nf 1803  df-nfc 2910

This theorem is referenced by:  nfeld  2934  ralcom2  3363  cbvexeqsetf  3468  sbcralt  3825  sbcrext  3826  csbie2t  3890  sbcco3gw  4378  sbcco3g  4383  csbco3g  4384  dfnfc2  4886  eusvnfb  5349  eusv2i  5350  dfid3  5543  iota2d  6505  iota2  6506  fmptcof  7108  nfriotadw  7357  riotaeqimp  7375  riota5f  7377  riota5  7378  oprabid  7424  opiota  8036  fmpoco  8069  nfttrcld  9662  axrepndlem1  10547  axrepndlem2  10548  axunnd  10551  axpowndlem2  10553  axpowndlem3  10554  axpowndlem4  10555  axpownd  10556  axregndlem2  10558  axinfndlem1  10560  axinfnd  10561  axacndlem4  10565  axacndlem5  10566  axacnd  10567  nfnegd  11422  prodsn  15975  fprodeq0g  16007  bpolylem  16061  pcmpt  16911  nfchnd  18626  chfacfpmmulfsupp  22903  elmptrab  23867  dvfsumrlim3  26075  itgsubstlem  26090  itgsubst  26091  ifeqeqx  32690  disjunsn  32743  axsepg2  35400  axnulg  35405  axpowg2  35407  axpowg3  35408  bj-elgab  37388  bj-gabima  37389  wl-issetft  38049  unirep  38177  riotasv2d  39545  cdleme31so  40967  cdleme31se  40970  cdleme31sc  40972  cdleme31sde  40973  cdleme31sn2  40977  cdlemeg47rv2  41098  cdlemk41  41508  mapdheq  42316  hdmap1eq  42389  hdmapval2lem  42419  monotuz  43482  oddcomabszz  43485  mnringvald  44753  nfxnegd  45979  fprodsplit1  46133  dvnmul  46481  sge0sn  46917  hoidmvlelem3  47135