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.

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

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