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

Theorem nfcvf2 2595
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 2594 . 2  |-  ( -. 
A. y  y  =  x  ->  F/_ y x )
21naecoms 2037 1  |-  ( -. 
A. x  x  =  y  ->  F/_ y x )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1549   F/_wnfc 2559
This theorem is referenced by:  dfid3  4499  oprabid  6105  axrepndlem1  8467  axrepndlem2  8468  axrepnd  8469  axunnd  8471  axpowndlem2  8473  axpowndlem3  8474  axpowndlem4  8475  axpownd  8476  axregndlem2  8478  axinfndlem1  8480  axinfnd  8481  axacndlem4  8485  axacndlem5  8486  axacnd  8487
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 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-cleq 2429  df-clel 2432  df-nfc 2561
  Copyright terms: Public domain W3C validator