Theorem nfcvf2 2949

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

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

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 2401

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 2909

This theorem is used by:  dfid3  5553  oprabid  7445  axrepndlem1  10601  axrepndlem2  10602  axrepnd  10603  axunnd  10605  axpowndlem3  10608  axpowndlem4  10609  axpownd  10610  axregndlem2  10612  axinfndlem1  10614  axinfnd  10615  axacndlem4  10619  axacndlem5  10620  axacnd  10621  bj-nfcsym  37642