Theorem nfcvf 2918

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1538  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-13 2370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-nfc 2878

This theorem is referenced by:  nfcvf2  2919  nfrald  3335  ralcom2  3340  nfrmod  3390  nfreud  3391  nfrmo  3392  nfdisj  5072  nfcvb  5315  nfriotad  7317  nfixp  8844  axextnd  10485  axrepndlem2  10487  axrepnd  10488  axunndlem1  10489  axunnd  10490  axpowndlem2  10492  axpowndlem4  10494  axregndlem2  10497  axregnd  10498  axinfndlem1  10499  axinfnd  10500  axacndlem4  10504  axacndlem5  10505  axacnd  10506  axsepg2  35049  axsepg2ALT  35050  axnulg  35059  axextdist  35773  bj-nfcsym  36873