Theorem nfcvf 2952

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 2926 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 1949	. 2 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑦
2		nfv 1949	. . 3 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧
3		elequ2 2162	. . 3 ⊢ (𝑧 = 𝑦 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑦))
4	2, 3	dvelimnf 2485	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦)
5	1, 4	nfcd 2919	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-13 2404

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 2913

This theorem is used by:  nfcvf2  2953  nfrald  3361  ralcom2  3366  nfrmod  3412  nfreud  3413  nfrmo  3414  nfdisj  5088  nfcvb  5345  nfriotad  7419  nfixp  8983  axextnd  10715  axrepndlem2  10717  axrepnd  10718  axunndlem1  10719  axunnd  10720  axpowndlem2  10722  axpowndlem4  10724  axregndlem2  10727  axregnd  10728  axinfndlem1  10729  axinfnd  10730  axacndlem4  10734  axacndlem5  10735  axacnd  10736  axsepg2  35949  axsepg3  35950  axsepg3ALT  35951  axsepg5  35953  axnulg  35954  axpowg2  35956  axpowg3  35957  axextdist  36776  bj-nfcsym  38026