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 1567  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-nfc 2909

This theorem is used by:  dfid3  5549  oprabid  7456  axrepndlem1  10684  axrepndlem2  10685  axrepnd  10686  axunnd  10688  axpowndlem3  10691  axpowndlem4  10692  axpownd  10693  axregndlem2  10695  axinfndlem1  10697  axinfnd  10698  axacndlem4  10702  axacndlem5  10703  axacnd  10704  bj-nfcsym  37935