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

Theorem nfcvd 2495
Description: If  x is disjoint from  A, then  x is not free in  A. (Contributed by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfcvd  |-  ( ph  -> 
F/_ x A )
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem nfcvd
StepHypRef Expression
1 nfcv 2494 . 2  |-  F/_ x A
21a1i 10 1  |-  ( ph  -> 
F/_ x A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/_wnfc 2481
This theorem is referenced by:  nfeld  2509  ralcom2  2780  vtoclgft  2910  vtocld  2912  sbcralt  3139  sbcrext  3140  csbied  3199  csbie2t  3201  sbcco3g  3212  csbco3g  3214  dfnfc2  3926  dfid3  4392  eusvnfb  4612  eusv2i  4613  nfiotad  5304  iota2d  5326  iota2  5327  fmptcof  5775  oprabid  5969  fmpt2co  6289  opiota  6377  nfriotad  6400  riota5f  6416  riota5  6417  riotasvdOLD  6435  riotasv2d  6436  riotasv2dOLD  6437  riotasv3dOLD  6441  axextnd  8303  axrepndlem1  8304  axrepndlem2  8305  axunndlem1  8307  axunnd  8308  axpowndlem2  8310  axpowndlem3  8311  axpowndlem4  8312  axpownd  8313  axregndlem2  8315  axregnd  8316  axinfndlem1  8317  axinfnd  8318  axacndlem4  8322  axacndlem5  8323  axacnd  8324  nfnegd  9137  sumsn  12310  pcmpt  13037  elmptrab  17624  dvfsumrlim3  19484  itgsubstlem  19499  itgsubst  19500  ifeqeqx  23200  prodsn  24587  axextdist  24714  bpolylem  25342  unirep  25673  monotuz  26349  oddcomabszz  26352  cdleme31so  30637  cdleme31se  30640  cdleme31sc  30642  cdleme31sde  30643  cdleme31sn2  30647  cdlemeg47rv2  30768  cdlemg1a  30828  cdlemk41  31178  mapdheq  31987  hdmap1eq  32061  hdmapval2lem  32093
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-nf 1545  df-nfc 2483
  Copyright terms: Public domain W3C validator