Theorem nfcvf 2921

Description: If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2372. See nfcv 2894 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 2703. (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 2453	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦)
5	1, 4	nfcd 2887	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1539  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-13 2372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-nfc 2881

This theorem is referenced by:  nfcvf2  2922  nfrald  3338  ralcom2  3343  nfrmod  3391  nfreud  3392  nfrmo  3393  nfdisj  5069  nfcvb  5312  nfriotad  7314  nfixp  8841  axextnd  10482  axrepndlem2  10484  axrepnd  10485  axunndlem1  10486  axunnd  10487  axpowndlem2  10489  axpowndlem4  10491  axregndlem2  10494  axregnd  10495  axinfndlem1  10496  axinfnd  10497  axacndlem4  10501  axacndlem5  10502  axacnd  10503  axsepg2  35094  axsepg2ALT  35095  axnulg  35119  axextdist  35841  bj-nfcsym  36941