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

Theorem nfcvf2 2608
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 2607 . 2  |-  ( -. 
A. y  y  =  x  ->  F/_ y x )
21naecoms 2106 1  |-  ( -. 
A. x  x  =  y  ->  F/_ y x )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1435   F/_wnfc 2568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2412  df-clel 2415  df-nfc 2570
This theorem is referenced by:  dfid3  4761  oprabid  6323  axrepndlem1  9006  axrepndlem2  9007  axrepnd  9008  axunnd  9010  axpowndlem3  9013  axpowndlem4  9014  axpownd  9015  axregndlem2  9017  axinfndlem1  9019  axinfnd  9020  axacndlem4  9024  axacndlem5  9025  axacnd  9026  bj-nfcsym  31285
  Copyright terms: Public domain W3C validator