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

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

Proof of Theorem nfcvf
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 nfcv 2613 . 2  |-  F/_ x
z
2 nfcv 2613 . 2  |-  F/_ z
y
3 id 22 . 2  |-  ( z  =  y  ->  z  =  y )
41, 2, 3dvelimc 2636 1  |-  ( -. 
A. x  x  =  y  ->  F/_ x y )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1368   F/_wnfc 2599
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 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-cleq 2443  df-clel 2446  df-nfc 2601
This theorem is referenced by:  nfcvf2  2638  nfrald  2878  ralcom2  2983  nfreud  2991  nfrmod  2992  nfrmo  2994  nfdisj  4374  nfcvb  4622  nfiotad  5484  nfriotad  6161  nfixp  7384  axextnd  8858  axrepndlem1  8859  axrepndlem2  8860  axrepnd  8861  axunndlem1  8862  axunnd  8863  axpowndlem2  8865  axpowndlem2OLD  8866  axpowndlem4  8869  axregndlem2  8872  axregnd  8873  axregndOLD  8874  axinfndlem1  8875  axinfnd  8876  axacndlem4  8880  axacndlem5  8881  axacnd  8882  axextdist  27749  bj-nfcsym  32697
  Copyright terms: Public domain W3C validator