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

Theorem nfcvd 2545
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 2544 . 2  |-  F/_ x A
21a1i 11 1  |-  ( ph  -> 
F/_ x A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/_wnfc 2531
This theorem is referenced by:  nfeld  2559  ralcom2  2836  vtoclgft  2966  vtocld  2968  sbcralt  3197  sbcrext  3198  csbied  3257  csbie2t  3259  sbcco3g  3269  csbco3g  3271  dfnfc2  3997  dfid3  4463  eusvnfb  4682  eusv2i  4683  nfiotad  5384  iota2d  5406  iota2  5407  fmptcof  5865  oprabid  6068  fmpt2co  6393  opiota  6498  nfriotad  6521  riota5f  6537  riota5  6538  riotasvdOLD  6556  riotasv2d  6557  riotasv2dOLD  6558  riotasv3dOLD  6562  axrepndlem1  8427  axrepndlem2  8428  axunnd  8431  axpowndlem2  8433  axpowndlem3  8434  axpowndlem4  8435  axpownd  8436  axregndlem2  8438  axinfndlem1  8440  axinfnd  8441  axacndlem4  8445  axacndlem5  8446  axacnd  8447  nfnegd  9261  sumsn  12493  pcmpt  13220  elmptrab  17816  dvfsumrlim3  19874  itgsubstlem  19889  itgsubst  19890  ifeqeqx  23958  prodsn  25243  bpolylem  26002  unirep  26308  monotuz  26898  oddcomabszz  26901  cdleme31so  30865  cdleme31se  30868  cdleme31sc  30870  cdleme31sde  30871  cdleme31sn2  30875  cdlemeg47rv2  30996  cdlemk41  31406  mapdheq  32215  hdmap1eq  32289  hdmapval2lem  32321
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-nf 1551  df-nfc 2533
  Copyright terms: Public domain W3C validator