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

Theorem nfcvf 2965
Description: If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.)
Assertion
Ref Expression
nfcvf (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)

Proof of Theorem nfcvf
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nfcv 2941 . 2 𝑥𝑧
2 nfcv 2941 . 2 𝑧𝑦
3 id 22 . 2 (𝑧 = 𝑦𝑧 = 𝑦)
41, 2, 3dvelimc 2964 1 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1651  wnfc 2928
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-cleq 2792  df-clel 2795  df-nfc 2930
This theorem is referenced by:  nfcvf2  2966  nfrald  3125  ralcom2  3285  nfreud  3293  nfrmod  3294  nfrmo  3296  nfdisj  4823  nfcvb  5046  nfriotad  6847  nfixp  8167  axextnd  9701  axrepndlem2  9703  axrepnd  9704  axunndlem1  9705  axunnd  9706  axpowndlem2  9708  axpowndlem4  9710  axregndlem2  9713  axregnd  9714  axinfndlem1  9715  axinfnd  9716  axacndlem4  9720  axacndlem5  9721  axacnd  9722  axextdist  32217  bj-nfcsym  33377
  Copyright terms: Public domain W3C validator