Theorem nfcvf 2927

Description: If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2366. See nfcv 2898 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 2698. (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 1910	. 2 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑦
2		nfv 1910	. . 3 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧
3		elequ2 2114	. . 3 ⊢ (𝑧 = 𝑦 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑦))
4	2, 3	dvelimnf 2447	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦)
5	1, 4	nfcd 2886	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1532  Ⅎwnfc 2878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-13 2366

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-nf 1779  df-nfc 2880

This theorem is referenced by:  nfcvf2  2928  nfrald  3363  ralcom2  3368  nfrmod  3423  nfreud  3424  nfrmo  3425  nfdisj  5120  nfcvb  5370  nfriotad  7382  nfixp  8927  axextnd  10606  axrepndlem2  10608  axrepnd  10609  axunndlem1  10610  axunnd  10611  axpowndlem2  10613  axpowndlem4  10615  axregndlem2  10618  axregnd  10619  axinfndlem1  10620  axinfnd  10621  axacndlem4  10625  axacndlem5  10626  axacnd  10627  axextdist  35331  bj-nfcsym  36313