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

Theorem nfcvf 3011
Description: If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ax-ext 2796. (Revised by Wolf Lammen, 10-May-2023.)
Assertion
Ref Expression
nfcvf (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)

Proof of Theorem nfcvf
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1908 . 2 𝑤 ¬ ∀𝑥 𝑥 = 𝑦
2 nfv 1908 . . 3 𝑥 𝑤𝑧
3 elequ2 2121 . . 3 (𝑧 = 𝑦 → (𝑤𝑧𝑤𝑦))
42, 3dvelimnf 2472 . 2 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤𝑦)
51, 4nfcd 2972 1 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1528  wnfc 2965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-13 2385
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-nfc 2967
This theorem is referenced by:  nfcvf2  3012  nfrald  3228  ralcom2  3368  nfreud  3377  nfrmod  3378  nfrmo  3382  nfdisj  5040  nfcvb  5273  nfriotad  7120  nfixp  8473  axextnd  10005  axrepndlem2  10007  axrepnd  10008  axunndlem1  10009  axunnd  10010  axpowndlem2  10012  axpowndlem4  10014  axregndlem2  10017  axregnd  10018  axinfndlem1  10019  axinfnd  10020  axacndlem4  10024  axacndlem5  10025  axacnd  10026  axextdist  32929  bj-nfcsym  34100
  Copyright terms: Public domain W3C validator