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

Theorem nfcvf 2773
Description: If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.)
Assertion
Ref Expression
nfcvf (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)

Proof of Theorem nfcvf
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nfcv 2750 . 2 𝑥𝑧
2 nfcv 2750 . 2 𝑧𝑦
3 id 22 . 2 (𝑧 = 𝑦𝑧 = 𝑦)
41, 2, 3dvelimc 2772 1 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1472  wnfc 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2602  df-clel 2605  df-nfc 2739
This theorem is referenced by:  nfcvf2  2774  nfrald  2927  ralcom2  3082  nfreud  3090  nfrmod  3091  nfrmo  3093  nfdisj  4559  nfcvb  4819  nfiotad  5757  nfriotad  6497  nfixp  7790  axextnd  9269  axrepndlem2  9271  axrepnd  9272  axunndlem1  9273  axunnd  9274  axpowndlem2  9276  axpowndlem4  9278  axregndlem2  9281  axregnd  9282  axinfndlem1  9283  axinfnd  9284  axacndlem4  9288  axacndlem5  9289  axacnd  9290  axextdist  30755  bj-nfcsym  31875
  Copyright terms: Public domain W3C validator