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

Theorem nfcvf 2937
Description: If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2373. See nfcv 2908 for a version that replaces the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ax-ext 2710. (Revised by Wolf Lammen, 10-May-2023.) (New usage is discouraged.)
Assertion
Ref Expression
nfcvf (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)

Proof of Theorem nfcvf
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1918 . 2 𝑤 ¬ ∀𝑥 𝑥 = 𝑦
2 nfv 1918 . . 3 𝑥 𝑤𝑧
3 elequ2 2122 . . 3 (𝑧 = 𝑦 → (𝑤𝑧𝑤𝑦))
42, 3dvelimnf 2454 . 2 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤𝑦)
51, 4nfcd 2896 1 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1537  wnfc 2888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-13 2373
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-nfc 2890
This theorem is referenced by:  nfcvf2  2938  nfrald  3151  ralcom2  3291  nfreud  3303  nfrmod  3304  nfrmo  3310  nfdisj  5053  nfcvb  5300  nfriotad  7253  nfixp  8714  axextnd  10356  axrepndlem2  10358  axrepnd  10359  axunndlem1  10360  axunnd  10361  axpowndlem2  10363  axpowndlem4  10365  axregndlem2  10368  axregnd  10369  axinfndlem1  10370  axinfnd  10371  axacndlem4  10375  axacndlem5  10376  axacnd  10377  axextdist  33784  bj-nfcsym  35093
  Copyright terms: Public domain W3C validator