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

Theorem nfcvf 2929
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 2900 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 2711. (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 1921 . 2 𝑤 ¬ ∀𝑥 𝑥 = 𝑦
2 nfv 1921 . . 3 𝑥 𝑤𝑧
3 elequ2 2129 . . 3 (𝑧 = 𝑦 → (𝑤𝑧𝑤𝑦))
42, 3dvelimnf 2454 . 2 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤𝑦)
51, 4nfcd 2888 1 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1540  wnfc 2880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-13 2373
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-nfc 2882
This theorem is referenced by:  nfcvf2  2930  nfrald  3138  ralcom2  3267  nfreud  3276  nfrmod  3277  nfrmo  3281  nfdisj  5009  nfcvb  5244  nfriotad  7142  nfixp  8530  axextnd  10094  axrepndlem2  10096  axrepnd  10097  axunndlem1  10098  axunnd  10099  axpowndlem2  10101  axpowndlem4  10103  axregndlem2  10106  axregnd  10107  axinfndlem1  10108  axinfnd  10109  axacndlem4  10113  axacndlem5  10114  axacnd  10115  axextdist  33352  bj-nfcsym  34731
  Copyright terms: Public domain W3C validator