Theorem nfcvf 2938

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 2908 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 1913	. 2 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑦
2		nfv 1913	. . 3 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧
3		elequ2 2123	. . 3 ⊢ (𝑧 = 𝑦 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑦))
4	2, 3	dvelimnf 2461	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦)
5	1, 4	nfcd 2901	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1535  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-13 2380

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-nfc 2895

This theorem is referenced by:  nfcvf2  2939  nfrald  3380  ralcom2  3385  nfrmod  3439  nfreud  3440  nfrmo  3441  nfdisj  5146  nfcvb  5394  nfriotad  7416  nfixp  8975  axextnd  10660  axrepndlem2  10662  axrepnd  10663  axunndlem1  10664  axunnd  10665  axpowndlem2  10667  axpowndlem4  10669  axregndlem2  10672  axregnd  10673  axinfndlem1  10674  axinfnd  10675  axacndlem4  10679  axacndlem5  10680  axacnd  10681  axsepg2  35058  axsepg2ALT  35059  axnulg  35068  axextdist  35763  bj-nfcsym  36865