Theorem nfcvf 2625

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 2602	. 2 |- F/_ x z
2		nfcv 2602	. 2 |- F/_ z y
3		id 22	. 2 |- ( z = y -> z = y )
4	1, 2, 3	dvelimc 2624	1 |- ( -. A. x x = y -> F/_ x y )

Syntax hints:   -. wn 3   -> wi 4   A.wal 1452   F/_wnfc 2589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-cleq 2454  df-clel 2457  df-nfc 2591

This theorem is referenced by:  nfcvf2  2626  nfrald  2784  ralcom2  2966  nfreud  2974  nfrmod  2975  nfrmo  2977  nfdisj  4398  nfcvb  4643  nfiotad  5567  nfriotad  6284  nfixp  7566  axextnd  9041  axrepndlem2  9043  axrepnd  9044  axunndlem1  9045  axunnd  9046  axpowndlem2  9048  axpowndlem4  9050  axregndlem2  9053  axregnd  9054  axinfndlem1  9055  axinfnd  9056  axacndlem4  9060  axacndlem5  9061  axacnd  9062  axextdist  30494  bj-nfcsym  31538