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

Theorem nfcvd 2620
Description: If is disjoint from , then is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfcvd
Distinct variable group:   ,

Proof of Theorem nfcvd
StepHypRef Expression
1 nfcv 2619 . 2
21a1i 11 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  F/_wnfc 2605
This theorem is referenced by:  nfeld  2627  ralcom2  3022  vtoclgft  3157  vtocld  3159  sbcralt  3408  sbcrextOLD  3409  sbcrext  3410  csbied  3461  csbie2t  3463  sbcco3g  3843  csbco3g  3844  dfnfc2  4267  eusvnfb  4648  eusv2i  4649  dfid3  4801  nfiotad  5559  iota2d  5581  iota2  5582  fmptcof  6065  riota5f  6282  riota5  6283  oprabid  6323  opiota  6859  fmpt2co  6883  axrepndlem1  8988  axrepndlem2  8989  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axpownd  8999  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  nfnegd  9838  sumsn  13563  prodsn  13767  pcmpt  14411  chfacfpmmulfsupp  19364  elmptrab  20328  dvfsumrlim3  22434  itgsubstlem  22449  itgsubst  22450  ifeqeqx  27419  disjunsn  27453  bpolylem  29810  unirep  30203  monotuz  30877  oddcomabszz  30880  fprodsplit1  31599  fprodeq0g  31601  dvnmul  31740  riotasv2d  34688  cdleme31so  36105  cdleme31se  36108  cdleme31sc  36110  cdleme31sde  36111  cdleme31sn2  36115  cdlemeg47rv2  36236  cdlemk41  36646  mapdheq  37455  hdmap1eq  37529  hdmapval2lem  37561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-nf 1617  df-nfc 2607
  Copyright terms: Public domain W3C validator