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

Theorem nfcvf2 2642
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 2641 . 2  |-  ( -. 
A. y  y  =  x  ->  F/_ y x )
21naecoms 2013 1  |-  ( -. 
A. x  x  =  y  ->  F/_ y x )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1368   F/_wnfc 2602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-cleq 2446  df-clel 2449  df-nfc 2604
This theorem is referenced by:  dfid3  4748  oprabid  6227  axrepndlem1  8870  axrepndlem2  8871  axrepnd  8872  axunnd  8874  axpowndlem2OLD  8877  axpowndlem3  8878  axpowndlem3OLD  8879  axpowndlem4  8880  axpownd  8881  axregndlem2  8883  axinfndlem1  8886  axinfnd  8887  axacndlem4  8891  axacndlem5  8892  axacnd  8893  bj-nfcsym  32747
  Copyright terms: Public domain W3C validator