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  5053  nfcvb  5306  nfriotad  7325  nfixp  8856  axextnd  10506  axrepndlem2  10508  axrepnd  10509  axunndlem1  10510  axunnd  10511  axpowndlem2  10513  axpowndlem4  10515  axregndlem2  10518  axregnd  10519  axinfndlem1  10520  axinfnd  10521  axacndlem4  10525  axacndlem5  10526  axacnd  10527  axsepg2  35330  axsepg3  35331  axsepg3ALT  35332  axsepg5  35334  axnulg  35335  axpowg2  35337  axpowg3  35338  axextdist  36034  bj-nfcsym  37261