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

Theorem nfcvf 2630
Description: If  x and  y are distinct, then  x is not free in  y. (Contributed by Mario Carneiro, 8-Oct-2016.)
Assertion
Ref Expression
nfcvf  |-  ( -. 
A. x  x  =  y  ->  F/_ x y )

Proof of Theorem nfcvf
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 nfcv 2605 . 2  |-  F/_ x
z
2 nfcv 2605 . 2  |-  F/_ z
y
3 id 22 . 2  |-  ( z  =  y  ->  z  =  y )
41, 2, 3dvelimc 2629 1  |-  ( -. 
A. x  x  =  y  ->  F/_ x y )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1381   F/_wnfc 2591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-cleq 2435  df-clel 2438  df-nfc 2593
This theorem is referenced by:  nfcvf2  2631  nfrald  2828  ralcom2  3008  nfreud  3016  nfrmod  3017  nfrmo  3019  nfdisj  4419  nfcvb  4667  nfiotad  5544  nfriotad  6250  nfixp  7490  axextnd  8969  axrepndlem2  8971  axrepnd  8972  axunndlem1  8973  axunnd  8974  axpowndlem2  8976  axpowndlem2OLD  8977  axpowndlem4  8980  axregndlem2  8983  axregnd  8984  axregndOLD  8985  axinfndlem1  8986  axinfnd  8987  axacndlem4  8991  axacndlem5  8992  axacnd  8993  axextdist  29208  bj-nfcsym  34343
  Copyright terms: Public domain W3C validator