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

Theorem nfcvd 2573
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 2572 . 2  |-  F/_ x A
21a1i 11 1  |-  ( ph  -> 
F/_ x A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/_wnfc 2559
This theorem is referenced by:  nfeld  2587  ralcom2  2872  vtoclgft  3002  vtocld  3004  sbcralt  3233  sbcrext  3234  csbied  3293  csbie2t  3295  sbcco3g  3305  csbco3g  3307  dfnfc2  4033  dfid3  4499  eusvnfb  4719  eusv2i  4720  nfiotad  5421  iota2d  5443  iota2  5444  fmptcof  5902  oprabid  6105  fmpt2co  6430  opiota  6535  nfriotad  6558  riota5f  6574  riota5  6575  riotasvdOLD  6593  riotasv2d  6594  riotasv2dOLD  6595  riotasv3dOLD  6599  axrepndlem1  8467  axrepndlem2  8468  axunnd  8471  axpowndlem2  8473  axpowndlem3  8474  axpowndlem4  8475  axpownd  8476  axregndlem2  8478  axinfndlem1  8480  axinfnd  8481  axacndlem4  8485  axacndlem5  8486  axacnd  8487  nfnegd  9301  sumsn  12534  pcmpt  13261  elmptrab  17859  dvfsumrlim3  19917  itgsubstlem  19932  itgsubst  19933  ifeqeqx  24001  prodsn  25286  bpolylem  26094  unirep  26414  monotuz  27004  oddcomabszz  27007  cdleme31so  31176  cdleme31se  31179  cdleme31sc  31181  cdleme31sde  31182  cdleme31sn2  31186  cdlemeg47rv2  31307  cdlemk41  31717  mapdheq  32526  hdmap1eq  32600  hdmapval2lem  32632
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-nf 1554  df-nfc 2561
  Copyright terms: Public domain W3C validator