Theorem dveel2 1355

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 969	. 2 |- (z e. w -> A.x z e. w)
2		ax-17 969	. 2 |- (z e. y -> A.w z e. y)
3		elequ2 1135	. 2 |- (w = y -> (z e. w <-> z e. y))
4	1, 2, 3	dvelimfALT 1151	1 |- (-. A.x x = y -> (z e. y -> A.x z e. y))

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

This theorem is referenced by:  ax15 1357  dfid3 2831  axextnd 4923  axrepndlem1 4924  axrepndlem2 4925  axunndlem1 4927  axunnd 4928  axpowndlem2 4930  axpowndlem3 4931  axpowndlem4 4932  axregndlem2 4935  axregnd 4936  axinfnd 4938  axacndlem5 4943  axacnd 4944

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138

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

Copyright terms: Public domain