Theorem nfcvf 2950

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1558  Ⅎwnfc 2909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-13 2403

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-nfc 2911

This theorem is referenced by:  nfcvf2  2951  nfrald  3359  ralcom2  3364  nfrmod  3410  nfreud  3411  nfrmo  3412  nfdisj  5080  nfcvb  5333  nfriotad  7364  nfixp  8899  axextnd  10549  axrepndlem2  10551  axrepnd  10552  axunndlem1  10553  axunnd  10554  axpowndlem2  10556  axpowndlem4  10558  axregndlem2  10561  axregnd  10562  axinfndlem1  10563  axinfnd  10564  axacndlem4  10568  axacndlem5  10569  axacnd  10570  axsepg2  35433  axsepg3  35434  axsepg3ALT  35435  axsepg5  35437  axnulg  35438  axpowg2  35440  axpowg3  35441  axextdist  36144  bj-nfcsym  37381