MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcvd Structured version   Visualization version   GIF version

Theorem nfcvd 2983
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
StepHypRef Expression
1 nfcv 2982 . 2 𝑥𝐴
21a1i 11 1 (𝜑𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnfc 2966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-ex 1774  df-nf 1778  df-nfc 2968
This theorem is referenced by:  nfeld  2994  nfraldw  3228  ralcom2  3369  nfreuw  3380  nfrmow  3381  vtoclgft  3559  vtoclgftOLD  3560  vtocld  3562  sbcralt  3859  sbcrext  3860  csbied  3923  csbie2t  3925  sbcco3gw  4378  sbcco3g  4383  csbco3g  4384  dfnfc2  4855  nfdisjw  5040  eusvnfb  5290  eusv2i  5291  dfid3  5461  iota2d  6341  iota2  6342  fmptcof  6888  nfriotadw  7114  riotaeqimp  7132  riota5f  7134  riota5  7135  oprabid  7180  opiota  7748  fmpoco  7781  axrepndlem1  10003  axrepndlem2  10004  axunnd  10007  axpowndlem2  10009  axpowndlem3  10010  axpowndlem4  10011  axpownd  10012  axregndlem2  10014  axinfndlem1  10016  axinfnd  10017  axacndlem4  10021  axacndlem5  10022  axacnd  10023  nfnegd  10870  prodsn  15306  fprodeq0g  15338  bpolylem  15392  pcmpt  16218  chfacfpmmulfsupp  21387  elmptrab  22351  dvfsumrlim3  24545  itgsubstlem  24560  itgsubst  24561  ifeqeqx  30211  disjunsn  30259  unirep  34856  riotasv2d  35960  cdleme31so  37382  cdleme31se  37385  cdleme31sc  37387  cdleme31sde  37388  cdleme31sn2  37392  cdlemeg47rv2  37513  cdlemk41  37923  mapdheq  38731  hdmap1eq  38804  hdmapval2lem  38834  monotuz  39403  oddcomabszz  39406  nfxnegd  41580  fprodsplit1  41739  dvnmul  42093  sge0sn  42527  hoidmvlelem3  42745
  Copyright terms: Public domain W3C validator