Theorem ddeel2 1004

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

Assertion

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

Distinct variable group(s):   x,z

Proof of Theorem ddeel2

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (z e. w -> A.x z e. w)
2		a14b 820	. 2 |- (w = y -> (z e. w <-> z e. y))
3	1, 2	ddelim 1000	1 |- (-. A.x x = y -> (z e. y -> A.x z e. y))

Syntax hints:  -. wn 1   -> wi 2  A.wal 672   = weq 797   e. wel 803

This theorem is referenced by:  ax15 1006  axextnd 3737  axrepndlem1 3738  axrepndlem2 3739  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregndlem2 3749  axregnd 3750  axinfnd 3752  axacndlem5 3757  axacnd 3758

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-14 805  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853

metamath.org