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

Theorem nfcvf 2593
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 2571 . 2  |-  F/_ x
z
2 nfcv 2571 . 2  |-  F/_ z
y
3 id 20 . 2  |-  ( z  =  y  ->  z  =  y )
41, 2, 3dvelimc 2592 1  |-  ( -. 
A. x  x  =  y  ->  F/_ x y )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1549   F/_wnfc 2558
This theorem is referenced by:  nfcvf2  2594  nfrald  2749  ralcom2  2864  nfreud  2872  nfrmod  2873  nfrmo  2875  nfdisj  4186  nfcvb  4386  nfiotad  5413  nfriotad  6550  nfixp  7073  axextnd  8456  axrepndlem1  8457  axrepndlem2  8458  axrepnd  8459  axunndlem1  8460  axunnd  8461  axpowndlem2  8463  axpowndlem4  8465  axregndlem2  8468  axregnd  8469  axinfndlem1  8470  axinfnd  8471  axacndlem4  8475  axacndlem5  8476  axacnd  8477  axextdist  25415
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-cleq 2428  df-clel 2431  df-nfc 2560
  Copyright terms: Public domain W3C validator