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

Theorem nfcvf2 2923
Description: If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. Usage of this theorem is discouraged because it depends on ax-13 2366. See nfcv 2892 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 2922 . 2 (¬ ∀𝑦 𝑦 = 𝑥𝑦𝑥)
21naecoms 2423 1 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1532  wnfc 2876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-13 2366
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-nf 1779  df-nfc 2878
This theorem is referenced by:  dfid3  5583  oprabid  7456  axrepndlem1  10635  axrepndlem2  10636  axrepnd  10637  axunnd  10639  axpowndlem3  10642  axpowndlem4  10643  axpownd  10644  axregndlem2  10646  axinfndlem1  10648  axinfnd  10649  axacndlem4  10653  axacndlem5  10654  axacnd  10655  bj-nfcsym  36605
  Copyright terms: Public domain W3C validator