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

Theorem nfcvf2 2774
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 2773 . 2 (¬ ∀𝑦 𝑦 = 𝑥𝑦𝑥)
21naecoms 2300 1 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1472  wnfc 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2602  df-clel 2605  df-nfc 2739
This theorem is referenced by:  dfid3  4944  oprabid  6554  axrepndlem1  9270  axrepndlem2  9271  axrepnd  9272  axunnd  9274  axpowndlem3  9277  axpowndlem4  9278  axpownd  9279  axregndlem2  9281  axinfndlem1  9283  axinfnd  9284  axacndlem4  9288  axacndlem5  9289  axacnd  9290  bj-nfcsym  31875
  Copyright terms: Public domain W3C validator