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

Theorem nfcvd 2420
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 2419 . 2  |-  F/_ x A
21a1i 10 1  |-  ( ph  -> 
F/_ x A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/_wnfc 2406
This theorem is referenced by:  nfeld  2434  ralcom2  2704  vtoclgft  2834  vtocld  2836  sbcralt  3063  sbcrext  3064  csbied  3123  csbie2t  3125  sbcco3g  3136  csbco3g  3138  dfnfc2  3845  dfid3  4310  eusvnfb  4530  eusv2i  4531  nfiotad  5222  iota2d  5244  iota2  5245  fmptcof  5692  oprabid  5882  fmpt2co  6202  opiota  6290  nfriotad  6313  riota5f  6329  riota5  6330  riotasvdOLD  6348  riotasv2d  6349  riotasv2dOLD  6350  riotasv3dOLD  6354  axextnd  8213  axrepndlem1  8214  axrepndlem2  8215  axunndlem1  8217  axunnd  8218  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axpownd  8223  axregndlem2  8225  axregnd  8226  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234  nfnegd  9047  sumsn  12213  pcmpt  12940  elmptrab  17522  dvfsumrlim3  19380  itgsubstlem  19395  itgsubst  19396  ifeqeqx  23034  axextdist  24156  bpolylem  24783  unirep  26349  monotuz  27026  oddcomabszz  27029  cdleme31so  30568  cdleme31se  30571  cdleme31sc  30573  cdleme31sde  30574  cdleme31sn2  30578  cdlemeg47rv2  30699  cdlemg1a  30759  cdlemk41  31109  mapdheq  31918  hdmap1eq  31992  hdmapval2lem  32024
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-nf 1532  df-nfc 2408
  Copyright terms: Public domain W3C validator