Theorem nfcvf 2788

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1481  Ⅎwnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753

This theorem is referenced by:  nfcvf2  2789  nfrald  2944  ralcom2  3104  nfreud  3112  nfrmod  3113  nfrmo  3115  nfdisj  4632  nfcvb  4898  nfriotad  6619  nfixp  7927  axextnd  9413  axrepndlem2  9415  axrepnd  9416  axunndlem1  9417  axunnd  9418  axpowndlem2  9420  axpowndlem4  9422  axregndlem2  9425  axregnd  9426  axinfndlem1  9427  axinfnd  9428  axacndlem4  9432  axacndlem5  9433  axacnd  9434  axextdist  31705  bj-nfcsym  32886