Theorem nfcvf 2630

Description: If x and y are distinct, then x is not free in y. (Contributed by Mario Carneiro, 8-Oct-2016.)

Assertion

Ref	Expression
nfcvf	|- ( -. A. x x = y -> F/_ x y )

Proof of Theorem nfcvf

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfcv 2605	. 2 |- F/_ x z
2		nfcv 2605	. 2 |- F/_ z y
3		id 22	. 2 |- ( z = y -> z = y )
4	1, 2, 3	dvelimc 2629	1 |- ( -. A. x x = y -> F/_ x y )

Syntax hints:   -. wn 3   -> wi 4   A.wal 1381   F/_wnfc 2591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-cleq 2435  df-clel 2438  df-nfc 2593

This theorem is referenced by:  nfcvf2  2631  nfrald  2828  ralcom2  3008  nfreud  3016  nfrmod  3017  nfrmo  3019  nfdisj  4419  nfcvb  4667  nfiotad  5544  nfriotad  6250  nfixp  7490  axextnd  8969  axrepndlem2  8971  axrepnd  8972  axunndlem1  8973  axunnd  8974  axpowndlem2  8976  axpowndlem2OLD  8977  axpowndlem4  8980  axregndlem2  8983  axregnd  8984  axregndOLD  8985  axinfndlem1  8986  axinfnd  8987  axacndlem4  8991  axacndlem5  8992  axacnd  8993  axextdist  29208  bj-nfcsym  34343