Theorem nfcvf2 2927

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540  Ⅎwnfc 2884

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-13 2377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-nfc 2886

This theorem is referenced by:  dfid3  5530  oprabid  7400  axrepndlem1  10515  axrepndlem2  10516  axrepnd  10517  axunnd  10519  axpowndlem3  10522  axpowndlem4  10523  axpownd  10524  axregndlem2  10526  axinfndlem1  10528  axinfnd  10529  axacndlem4  10533  axacndlem5  10534  axacnd  10535  bj-nfcsym  37147