Theorem nfcvf2 2938

Description: If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. (Contributed by Mario Carneiro, 5-Dec-2016.)

Assertion

Ref	Expression
nfcvf2	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)

Proof of Theorem nfcvf2

Step	Hyp	Ref	Expression
1		nfcvf 2937	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦𝑥)
2	1	naecoms 2465	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1629  Ⅎwnfc 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-cleq 2764  df-clel 2767  df-nfc 2902

This theorem is referenced by:  dfid3  5158  oprabid  6822  axrepndlem1  9616  axrepndlem2  9617  axrepnd  9618  axunnd  9620  axpowndlem3  9623  axpowndlem4  9624  axpownd  9625  axregndlem2  9627  axinfndlem1  9629  axinfnd  9630  axacndlem4  9634  axacndlem5  9635  axacnd  9636  bj-nfcsym  33215