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

Theorem nfcvf2 3002
 Description: If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. Usage of this theorem is discouraged because it depends on ax-13 2391. See nfcv 2974 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 3001 . 2 (¬ ∀𝑦 𝑦 = 𝑥𝑦𝑥)
21naecoms 2452 1 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1536  Ⅎwnfc 2958 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 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-13 2391 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-nfc 2960 This theorem is referenced by:  dfid3  5435  oprabid  7162  axrepndlem1  9991  axrepndlem2  9992  axrepnd  9993  axunnd  9995  axpowndlem3  9998  axpowndlem4  9999  axpownd  10000  axregndlem2  10002  axinfndlem1  10004  axinfnd  10005  axacndlem4  10009  axacndlem5  10010  axacnd  10011  bj-nfcsym  34231
 Copyright terms: Public domain W3C validator