Theorem nfcvf 2929

Description: If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2373. See nfcv 2900 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 2129	. . 3 ⊢ (𝑧 = 𝑦 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑦))
4	2, 3	dvelimnf 2454	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦)
5	1, 4	nfcd 2888	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540  Ⅎwnfc 2880

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 1975  ax-7 2020  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-13 2373

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-nfc 2882

This theorem is referenced by:  nfcvf2  2930  nfrald  3138  ralcom2  3267  nfreud  3276  nfrmod  3277  nfrmo  3281  nfdisj  5009  nfcvb  5244  nfriotad  7142  nfixp  8530  axextnd  10094  axrepndlem2  10096  axrepnd  10097  axunndlem1  10098  axunnd  10099  axpowndlem2  10101  axpowndlem4  10103  axregndlem2  10106  axregnd  10107  axinfndlem1  10108  axinfnd  10109  axacndlem4  10113  axacndlem5  10114  axacnd  10115  axextdist  33352  bj-nfcsym  34731