Theorem dveel2 1357

Description: Quantifier introduction when one pair of variables is distinct.

Assertion

Ref	Expression
dveel2	|- (-. A.x x = y -> (z e. y -> A.x z e. y))

Distinct variable group:   x,z

Proof of Theorem dveel2

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (z e. w -> A.x z e. w)
2		ax-17 971	. 2 |- (z e. y -> A.w z e. y)
3		elequ2 1137	. 2 |- (w = y -> (z e. w <-> z e. y))
4	1, 2, 3	dvelimfALT 1153	1 |- (-. A.x x = y -> (z e. y -> A.x z e. y))

Syntax hints:  -. wn 2   -> wi 3  A.wal 954   = wceq 956   e. wcel 958

This theorem is referenced by:  ax15 1359  dfid3 2836  axextnd 4943  axrepndlem1 4944  axrepndlem2 4945  axunndlem1 4947  axunnd 4948  axpowndlem2 4950  axpowndlem3 4951  axpowndlem4 4952  axregndlem2 4955  axregnd 4956  axinfnd 4958  axacndlem5 4963  axacnd 4964

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain