Theorem nfcvf 2931

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1537  Ⅎwnfc 2889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-13 2376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-nfc 2891

This theorem is referenced by:  nfcvf2  2932  nfrald  3371  ralcom2  3376  nfrmod  3431  nfreud  3432  nfrmo  3433  nfdisj  5122  nfcvb  5375  nfriotad  7400  nfixp  8958  axextnd  10632  axrepndlem2  10634  axrepnd  10635  axunndlem1  10636  axunnd  10637  axpowndlem2  10639  axpowndlem4  10641  axregndlem2  10644  axregnd  10645  axinfndlem1  10646  axinfnd  10647  axacndlem4  10651  axacndlem5  10652  axacnd  10653  axsepg2  35097  axsepg2ALT  35098  axnulg  35107  axextdist  35801  bj-nfcsym  36901