Theorem nfcvf2 2950

Description: If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. Usage of this theorem is discouraged because it depends on ax-13 2402. See nfcv 2923 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 2949	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦𝑥)
2	1	naecoms 2459	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1568  Ⅎwnfc 2908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-13 2402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-nfc 2910

This theorem is used by:  dfid3  5549  oprabid  7450  axrepndlem1  10670  axrepndlem2  10671  axrepnd  10672  axunnd  10674  axpowndlem3  10677  axpowndlem4  10678  axpownd  10679  axregndlem2  10681  axinfndlem1  10683  axinfnd  10684  axacndlem4  10688  axacndlem5  10689  axacnd  10690  bj-nfcsym  37791