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

Theorem nfcvf2 2636
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 2635 . 2  |-  ( -. 
A. y  y  =  x  ->  F/_ y x )
21naecoms 2162 1  |-  ( -. 
A. x  x  =  y  ->  F/_ y x )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1450   F/_wnfc 2599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-cleq 2464  df-clel 2467  df-nfc 2601
This theorem is referenced by:  dfid3  4755  oprabid  6335  axrepndlem1  9035  axrepndlem2  9036  axrepnd  9037  axunnd  9039  axpowndlem3  9042  axpowndlem4  9043  axpownd  9044  axregndlem2  9046  axinfndlem1  9048  axinfnd  9049  axacndlem4  9053  axacndlem5  9054  axacnd  9055  bj-nfcsym  31562
  Copyright terms: Public domain W3C validator