Theorem nfcvf 2649

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

Syntax hints:   -. wn 3   -> wi 4   A.wal 1372   F/_wnfc 2610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-cleq 2454  df-clel 2457  df-nfc 2612

This theorem is referenced by:  nfcvf2  2650  nfrald  2844  ralcom2  3021  nfreud  3029  nfrmod  3030  nfrmo  3032  nfdisj  4424  nfcvb  4672  nfiotad  5547  nfriotad  6246  nfixp  7480  axextnd  8957  axrepndlem1  8958  axrepndlem2  8959  axrepnd  8960  axunndlem1  8961  axunnd  8962  axpowndlem2  8964  axpowndlem2OLD  8965  axpowndlem4  8968  axregndlem2  8971  axregnd  8972  axregndOLD  8973  axinfndlem1  8974  axinfnd  8975  axacndlem4  8979  axacndlem5  8980  axacnd  8981  axextdist  28797  bj-nfcsym  33418