Theorem nfcvf 2965

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.

Step	Hyp	Ref	Expression
1		nfcv 2941	. 2 ⊢ Ⅎ𝑥𝑧
2		nfcv 2941	. 2 ⊢ Ⅎ𝑧𝑦
3		id 22	. 2 ⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦)
4	1, 2, 3	dvelimc 2964	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1651  Ⅎwnfc 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-cleq 2792  df-clel 2795  df-nfc 2930

This theorem is referenced by:  nfcvf2  2966  nfrald  3125  ralcom2  3285  nfreud  3293  nfrmod  3294  nfrmo  3296  nfdisj  4823  nfcvb  5046  nfriotad  6847  nfixp  8167  axextnd  9701  axrepndlem2  9703  axrepnd  9704  axunndlem1  9705  axunnd  9706  axpowndlem2  9708  axpowndlem4  9710  axregndlem2  9713  axregnd  9714  axinfndlem1  9715  axinfnd  9716  axacndlem4  9720  axacndlem5  9721  axacnd  9722  axextdist  32217  bj-nfcsym  33377