Theorem nfcvf 2953

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1568  Ⅎwnfc 2912

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-13 2406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-nfc 2914

This theorem is used by:  nfcvf2  2954  nfrald  3363  ralcom2  3368  nfrmod  3414  nfreud  3415  nfrmo  3416  nfdisj  5091  nfcvb  5349  nfriotad  7387  nfixp  8921  axextnd  10591  axrepndlem2  10593  axrepnd  10594  axunndlem1  10595  axunnd  10596  axpowndlem2  10598  axpowndlem4  10600  axregndlem2  10603  axregnd  10604  axinfndlem1  10605  axinfnd  10606  axacndlem4  10610  axacndlem5  10611  axacnd  10612  axsepg2  35610  axsepg3  35611  axsepg3ALT  35612  axsepg5  35614  axnulg  35615  axpowg2  35617  axpowg3  35618  axextdist  36326  bj-nfcsym  37591