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

Theorem nfcvf 2441
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 2419 . 2  |-  F/_ x
z
2 nfcv 2419 . 2  |-  F/_ z
y
3 id 19 . 2  |-  ( z  =  y  ->  z  =  y )
41, 2, 3dvelimc 2440 1  |-  ( -. 
A. x  x  =  y  ->  F/_ x y )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1527    = wceq 1623   F/_wnfc 2406
This theorem is referenced by:  nfcvf2  2442  nfrald  2594  ralcom2  2704  nfreud  2712  nfrmod  2713  nfrmo  2715  nfdisj  4005  nfcvb  4205  nfiotad  5222  nfriotad  6313  nfixp  6835  axextnd  8213  axrepndlem1  8214  axrepndlem2  8215  axrepnd  8216  axunndlem1  8217  axunnd  8218  axpowndlem2  8220  axpowndlem4  8222  axregndlem2  8225  axregnd  8226  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234  axextdist  23567
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408
  Copyright terms: Public domain W3C validator