Theorem nfcvf 2957

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1565  Ⅎwnfc 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-13 2410

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-nfc 2918

This theorem is referenced by:  nfcvf2  2958  nfrald  3368  ralcom2  3373  nfrmod  3419  nfreud  3420  nfrmo  3421  nfdisj  5093  nfcvb  5348  nfriotad  7379  nfixp  8914  axextnd  10575  axrepndlem2  10577  axrepnd  10578  axunndlem1  10579  axunnd  10580  axpowndlem2  10582  axpowndlem4  10584  axregndlem2  10587  axregnd  10588  axinfndlem1  10589  axinfnd  10590  axacndlem4  10594  axacndlem5  10595  axacnd  10596  axsepg2  35475  axsepg3  35476  axsepg3ALT  35477  axsepg5  35479  axnulg  35480  axpowg2  35482  axpowg3  35483  axextdist  36187  bj-nfcsym  37422