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

Theorem nfcvf 2931
Description: If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2376. See nfcv 2904 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 2707. (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 1913 . 2 𝑤 ¬ ∀𝑥 𝑥 = 𝑦
2 nfv 1913 . . 3 𝑥 𝑤𝑧
3 elequ2 2122 . . 3 (𝑧 = 𝑦 → (𝑤𝑧𝑤𝑦))
42, 3dvelimnf 2457 . 2 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤𝑦)
51, 4nfcd 2897 1 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1537  wnfc 2889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-13 2376
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-nfc 2891
This theorem is referenced by:  nfcvf2  2932  nfrald  3371  ralcom2  3376  nfrmod  3431  nfreud  3432  nfrmo  3433  nfdisj  5122  nfcvb  5375  nfriotad  7400  nfixp  8958  axextnd  10632  axrepndlem2  10634  axrepnd  10635  axunndlem1  10636  axunnd  10637  axpowndlem2  10639  axpowndlem4  10641  axregndlem2  10644  axregnd  10645  axinfndlem1  10646  axinfnd  10647  axacndlem4  10651  axacndlem5  10652  axacnd  10653  axsepg2  35097  axsepg2ALT  35098  axnulg  35107  axextdist  35801  bj-nfcsym  36901
  Copyright terms: Public domain W3C validator