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

Theorem nfcvf 2547
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 2525 . 2  |-  F/_ x
z
2 nfcv 2525 . 2  |-  F/_ z
y
3 id 20 . 2  |-  ( z  =  y  ->  z  =  y )
41, 2, 3dvelimc 2546 1  |-  ( -. 
A. x  x  =  y  ->  F/_ x y )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1546   F/_wnfc 2512
This theorem is referenced by:  nfcvf2  2548  nfrald  2702  ralcom2  2817  nfreud  2825  nfrmod  2826  nfrmo  2828  nfdisj  4137  nfcvb  4337  nfiotad  5363  nfriotad  6496  nfixp  7019  axextnd  8401  axrepndlem1  8402  axrepndlem2  8403  axrepnd  8404  axunndlem1  8405  axunnd  8406  axpowndlem2  8408  axpowndlem4  8410  axregndlem2  8413  axregnd  8414  axinfndlem1  8415  axinfnd  8416  axacndlem4  8420  axacndlem5  8421  axacnd  8422  axextdist  25182
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2382  df-clel 2385  df-nfc 2514
  Copyright terms: Public domain W3C validator