Theorem nfcvf 2981

Description: If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2379. See nfcv 2955 for a version that replaces the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ax-ext 2770. (Revised by Wolf Lammen, 10-May-2023.) (New usage is discouraged.)

Assertion

Ref	Expression
nfcvf	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)

Proof of Theorem nfcvf

Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1915	. 2 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑦
2		nfv 1915	. . 3 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧
3		elequ2 2126	. . 3 ⊢ (𝑧 = 𝑦 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑦))
4	2, 3	dvelimnf 2464	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦)
5	1, 4	nfcd 2944	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1536  Ⅎwnfc 2936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-13 2379

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-nfc 2938

This theorem is referenced by:  nfcvf2  2982  nfrald  3188  ralcom2  3316  nfreud  3325  nfrmod  3326  nfrmo  3330  nfdisj  5008  nfcvb  5242  nfriotad  7104  nfixp  8464  axextnd  10002  axrepndlem2  10004  axrepnd  10005  axunndlem1  10006  axunnd  10007  axpowndlem2  10009  axpowndlem4  10011  axregndlem2  10014  axregnd  10015  axinfndlem1  10016  axinfnd  10017  axacndlem4  10021  axacndlem5  10022  axacnd  10023  axextdist  33157  bj-nfcsym  34339