Theorem nfcvf 2774

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 2751	. 2 ⊢ Ⅎ𝑥𝑧
2		nfcv 2751	. 2 ⊢ Ⅎ𝑧𝑦
3		id 22	. 2 ⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦)
4	1, 2, 3	dvelimc 2773	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1473  Ⅎwnfc 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740

This theorem is referenced by:  nfcvf2  2775  nfrald  2928  ralcom2  3083  nfreud  3091  nfrmod  3092  nfrmo  3094  nfdisj  4565  nfcvb  4824  nfiotad  5771  nfriotad  6519  nfixp  7813  axextnd  9292  axrepndlem2  9294  axrepnd  9295  axunndlem1  9296  axunnd  9297  axpowndlem2  9299  axpowndlem4  9301  axregndlem2  9304  axregnd  9305  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  axextdist  30949  bj-nfcsym  32079