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

Theorem nfcvf 2649
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 2624 . 2  |-  F/_ x
z
2 nfcv 2624 . 2  |-  F/_ z
y
3 id 22 . 2  |-  ( z  =  y  ->  z  =  y )
41, 2, 3dvelimc 2648 1  |-  ( -. 
A. x  x  =  y  ->  F/_ x y )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1372   F/_wnfc 2610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-cleq 2454  df-clel 2457  df-nfc 2612
This theorem is referenced by:  nfcvf2  2650  nfrald  2844  ralcom2  3021  nfreud  3029  nfrmod  3030  nfrmo  3032  nfdisj  4424  nfcvb  4672  nfiotad  5547  nfriotad  6246  nfixp  7480  axextnd  8957  axrepndlem1  8958  axrepndlem2  8959  axrepnd  8960  axunndlem1  8961  axunnd  8962  axpowndlem2  8964  axpowndlem2OLD  8965  axpowndlem4  8968  axregndlem2  8971  axregnd  8972  axregndOLD  8973  axinfndlem1  8974  axinfnd  8975  axacndlem4  8979  axacndlem5  8980  axacnd  8981  axextdist  28797  bj-nfcsym  33418
  Copyright terms: Public domain W3C validator