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

Theorem nfcvd 2630
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 2629 . 2  |-  F/_ x A
21a1i 11 1  |-  ( ph  -> 
F/_ x A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-nf 1600  df-nfc 2617
This theorem is referenced by:  nfeld  2637  ralcom2  3026  vtoclgft  3161  vtocld  3163  sbcralt  3412  sbcrextOLD  3413  sbcrext  3414  csbied  3462  csbie2t  3464  sbcco3g  3843  csbco3g  3844  dfnfc2  4263  eusvnfb  4643  eusv2i  4644  dfid3  4796  nfiotad  5554  iota2d  5576  iota2  5577  fmptcof  6055  riota5f  6270  riota5  6271  oprabid  6308  opiota  6843  fmpt2co  6866  axrepndlem1  8967  axrepndlem2  8968  axunnd  8971  axpowndlem2  8973  axpowndlem2OLD  8974  axpowndlem3  8975  axpowndlem3OLD  8976  axpowndlem4  8977  axpownd  8978  axregndlem2  8980  axinfndlem1  8983  axinfnd  8984  axacndlem4  8988  axacndlem5  8989  axacnd  8990  nfnegd  9815  sumsn  13526  pcmpt  14270  chfacfpmmulfsupp  19159  elmptrab  20091  dvfsumrlim3  22197  itgsubstlem  22212  itgsubst  22213  ifeqeqx  27121  disjunsn  27154  prodsn  28697  bpolylem  29415  unirep  29834  monotuz  30509  oddcomabszz  30512  riotasv2d  33778  cdleme31so  35193  cdleme31se  35196  cdleme31sc  35198  cdleme31sde  35199  cdleme31sn2  35203  cdlemeg47rv2  35324  cdlemk41  35734  mapdheq  36543  hdmap1eq  36617  hdmapval2lem  36649
  Copyright terms: Public domain W3C validator