Theorem nfcvf 2927

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1545  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-13 2380

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-nfc 2888

This theorem is referenced by:  nfcvf2  2928  nfrald  3336  ralcom2  3341  nfrmod  3387  nfreud  3388  nfrmo  3389  nfdisj  5052  nfcvb  5305  nfriotad  7324  nfixp  8855  axextnd  10505  axrepndlem2  10507  axrepnd  10508  axunndlem1  10509  axunnd  10510  axpowndlem2  10512  axpowndlem4  10514  axregndlem2  10517  axregnd  10518  axinfndlem1  10519  axinfnd  10520  axacndlem4  10524  axacndlem5  10525  axacnd  10526  axsepg2  35321  axsepg3  35322  axsepg3ALT  35323  axsepg5  35325  axnulg  35326  axpowg2  35328  axpowg3  35329  axextdist  36025  bj-nfcsym  37252