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

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

Proof of Theorem nfcvf2
StepHypRef Expression
1 nfcvf 2441 . 2  |-  ( -. 
A. y  y  =  x  ->  F/_ y x )
21naecoms 1888 1  |-  ( -. 
A. x  x  =  y  ->  F/_ y x )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1527   F/_wnfc 2406
This theorem is referenced by:  dfid3  4310  oprabid  5882  axrepndlem1  8214  axrepndlem2  8215  axrepnd  8216  axunnd  8218  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axpownd  8223  axregndlem2  8225  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234
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