Theorem nfcvd 2978

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

Syntax hints:   → wi 4  Ⅎwnfc 2961

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

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-nf 1785  df-nfc 2963

This theorem is referenced by:  nfeld  2989  nfraldw  3223  ralcom2  3363  nfreuw  3374  nfrmow  3375  vtoclgft  3553  vtoclgftOLD  3554  vtocld  3556  sbcralt  3855  sbcrext  3856  csbied  3919  csbie2t  3921  sbcco3gw  4374  sbcco3g  4379  csbco3g  4380  dfnfc2  4860  nfdisjw  5043  eusvnfb  5294  eusv2i  5295  dfid3  5462  iota2d  6343  iota2  6344  fmptcof  6892  nfriotadw  7122  riotaeqimp  7140  riota5f  7142  riota5  7143  oprabid  7188  opiota  7757  fmpoco  7790  axrepndlem1  10014  axrepndlem2  10015  axunnd  10018  axpowndlem2  10020  axpowndlem3  10021  axpowndlem4  10022  axpownd  10023  axregndlem2  10025  axinfndlem1  10027  axinfnd  10028  axacndlem4  10032  axacndlem5  10033  axacnd  10034  nfnegd  10881  prodsn  15316  fprodeq0g  15348  bpolylem  15402  pcmpt  16228  chfacfpmmulfsupp  21471  elmptrab  22435  dvfsumrlim3  24630  itgsubstlem  24645  itgsubst  24646  ifeqeqx  30297  disjunsn  30344  unirep  35003  riotasv2d  36108  cdleme31so  37530  cdleme31se  37533  cdleme31sc  37535  cdleme31sde  37536  cdleme31sn2  37540  cdlemeg47rv2  37661  cdlemk41  38071  mapdheq  38879  hdmap1eq  38952  hdmapval2lem  38982  monotuz  39558  oddcomabszz  39561  nfxnegd  41735  fprodsplit1  41894  dvnmul  42248  sge0sn  42681  hoidmvlelem3  42899