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

Theorem nfcvf 2625
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 2602 . 2  |-  F/_ x
z
2 nfcv 2602 . 2  |-  F/_ z
y
3 id 22 . 2  |-  ( z  =  y  ->  z  =  y )
41, 2, 3dvelimc 2624 1  |-  ( -. 
A. x  x  =  y  ->  F/_ x y )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1452   F/_wnfc 2589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-cleq 2454  df-clel 2457  df-nfc 2591
This theorem is referenced by:  nfcvf2  2626  nfrald  2784  ralcom2  2966  nfreud  2974  nfrmod  2975  nfrmo  2977  nfdisj  4398  nfcvb  4643  nfiotad  5567  nfriotad  6284  nfixp  7566  axextnd  9041  axrepndlem2  9043  axrepnd  9044  axunndlem1  9045  axunnd  9046  axpowndlem2  9048  axpowndlem4  9050  axregndlem2  9053  axregnd  9054  axinfndlem1  9055  axinfnd  9056  axacndlem4  9060  axacndlem5  9061  axacnd  9062  axextdist  30494  bj-nfcsym  31538
  Copyright terms: Public domain W3C validator