Theorem nfcvf 2948

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-nfc 2909

This theorem is used by:  nfcvf2  2949  nfrald  3357  ralcom2  3362  nfrmod  3408  nfreud  3409  nfrmo  3410  nfdisj  5082  nfcvb  5338  nfriotad  7392  nfixp  8952  axextnd  10683  axrepndlem2  10685  axrepnd  10686  axunndlem1  10687  axunnd  10688  axpowndlem2  10690  axpowndlem4  10692  axregndlem2  10695  axregnd  10696  axinfndlem1  10697  axinfnd  10698  axacndlem4  10702  axacndlem5  10703  axacnd  10704  axsepg2  35868  axsepg3  35869  axsepg3ALT  35870  axsepg5  35872  axnulg  35873  axpowg2  35875  axpowg3  35876  axextdist  36657  bj-nfcsym  37907