Theorem nfcvf2 2982

Description: If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. Usage of this theorem is discouraged because it depends on ax-13 2379. See nfcv 2955 for a version that replaces the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by Mario Carneiro, 5-Dec-2016.) (New usage is discouraged.)

Assertion

Ref	Expression
nfcvf2	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)

Proof of Theorem nfcvf2

Step	Hyp	Ref	Expression
1		nfcvf 2981	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦𝑥)
2	1	naecoms 2440	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1536  Ⅎwnfc 2936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-13 2379

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-nfc 2938

This theorem is referenced by:  dfid3  5427  oprabid  7167  axrepndlem1  10003  axrepndlem2  10004  axrepnd  10005  axunnd  10007  axpowndlem3  10010  axpowndlem4  10011  axpownd  10012  axregndlem2  10014  axinfndlem1  10016  axinfnd  10017  axacndlem4  10021  axacndlem5  10022  axacnd  10023  bj-nfcsym  34339