Theorem nfcvf 2951

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1568  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-13 2404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-nfc 2912

This theorem is referenced by:  nfcvf2  2952  nfrald  3361  ralcom2  3366  nfrmod  3412  nfreud  3413  nfrmo  3414  nfdisj  5089  nfcvb  5347  nfriotad  7378  nfixp  8911  axextnd  10571  axrepndlem2  10573  axrepnd  10574  axunndlem1  10575  axunnd  10576  axpowndlem2  10578  axpowndlem4  10580  axregndlem2  10583  axregnd  10584  axinfndlem1  10585  axinfnd  10586  axacndlem4  10590  axacndlem5  10591  axacnd  10592  axsepg2  35553  axsepg3  35554  axsepg3ALT  35555  axsepg5  35557  axnulg  35558  axpowg2  35560  axpowg3  35561  axextdist  36289  bj-nfcsym  37534