Theorem nfcvf2 2920

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1538  Ⅎwnfc 2877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-13 2371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-nfc 2879

This theorem is referenced by:  dfid3  5539  oprabid  7422  axrepndlem1  10552  axrepndlem2  10553  axrepnd  10554  axunnd  10556  axpowndlem3  10559  axpowndlem4  10560  axpownd  10561  axregndlem2  10563  axinfndlem1  10565  axinfnd  10566  axacndlem4  10570  axacndlem5  10571  axacnd  10572  bj-nfcsym  36894