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

Theorem nfcvf 2774
 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 2751 . 2 𝑥𝑧
2 nfcv 2751 . 2 𝑧𝑦
3 id 22 . 2 (𝑧 = 𝑦𝑧 = 𝑦)
41, 2, 3dvelimc 2773 1 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1473  Ⅎwnfc 2738 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740 This theorem is referenced by:  nfcvf2  2775  nfrald  2928  ralcom2  3083  nfreud  3091  nfrmod  3092  nfrmo  3094  nfdisj  4565  nfcvb  4824  nfiotad  5771  nfriotad  6519  nfixp  7813  axextnd  9292  axrepndlem2  9294  axrepnd  9295  axunndlem1  9296  axunnd  9297  axpowndlem2  9299  axpowndlem4  9301  axregndlem2  9304  axregnd  9305  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  axextdist  30949  bj-nfcsym  32079
 Copyright terms: Public domain W3C validator