Theorem nfcvf2 2953

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-13 2404

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 2913

This theorem is used by:  dfid3  5556  oprabid  7483  axrepndlem1  10716  axrepndlem2  10717  axrepnd  10718  axunnd  10720  axpowndlem3  10723  axpowndlem4  10724  axpownd  10725  axregndlem2  10727  axinfndlem1  10729  axinfnd  10730  axacndlem4  10734  axacndlem5  10735  axacnd  10736  bj-nfcsym  38026