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

Theorem nfcvf2 2933
Description: If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. Usage of this theorem is discouraged because it depends on ax-13 2371. See nfcv 2903 for a version that replaces the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by Mario Carneiro, 5-Dec-2016.) (New usage is discouraged.)
Assertion
Ref Expression
nfcvf2 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)

Proof of Theorem nfcvf2
StepHypRef Expression
1 nfcvf 2932 . 2 (¬ ∀𝑦 𝑦 = 𝑥𝑦𝑥)
21naecoms 2428 1 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1539  wnfc 2883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2371
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-nfc 2885
This theorem is referenced by:  dfid3  5577  oprabid  7440  axrepndlem1  10586  axrepndlem2  10587  axrepnd  10588  axunnd  10590  axpowndlem3  10593  axpowndlem4  10594  axpownd  10595  axregndlem2  10597  axinfndlem1  10599  axinfnd  10600  axacndlem4  10604  axacndlem5  10605  axacnd  10606  bj-nfcsym  35774
  Copyright terms: Public domain W3C validator