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

Theorem nfcvf2 2961
Description: If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. (Contributed by Mario Carneiro, 5-Dec-2016.)
Assertion
Ref Expression
nfcvf2 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)

Proof of Theorem nfcvf2
StepHypRef Expression
1 nfcvf 2960 . 2 (¬ ∀𝑦 𝑦 = 𝑥𝑦𝑥)
21naecoms 2395 1 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1599  wnfc 2919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-nfc 2921
This theorem is referenced by:  dfid3  5262  oprabid  6953  axrepndlem1  9749  axrepndlem2  9750  axrepnd  9751  axunnd  9753  axpowndlem3  9756  axpowndlem4  9757  axpownd  9758  axregndlem2  9760  axinfndlem1  9762  axinfnd  9763  axacndlem4  9767  axacndlem5  9768  axacnd  9769  bj-nfcsym  33457
  Copyright terms: Public domain W3C validator