Theorem ax15 1339

Description: Axiom ax-15 1109 is redundant if we assume ax-17 1190. Remark 9.6 in [Megill] p. 448 (p. 16 of the preprint), regarding axiom scheme C14'.

Note that w is a dummy variable introduced in the proof. On the web page, it is implicitly assumed to be distinct from all other variables. (This is made explicit in the database file set.mm). Its purpose is to satisfy the distinct variable requirements of dveel2 1337 and dvelim 1334. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements.

Assertion

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

Proof of Theorem ax15

Step	Hyp	Ref	Expression
1		hbn1 989	. . . . 5 |- (-. A.z z = y -> A.z -. A.z z = y)
2		dveel2 1337	. . . . 5 |- (-. A.z z = y -> (w e. y -> A.z w e. y))
3	1, 2	hbim1 1079	. . . 4 |- ((-. A.z z = y -> w e. y) -> A.z(-. A.z z = y -> w e. y))
4		ax-17 1190	. . . 4 |- ((-. A.z z = y -> x e. y) -> A.w(-. A.z z = y -> x e. y))
5		elequ1 1123	. . . . 5 |- (w = x -> (w e. y <-> x e. y))
6	5	imbi2d 610	. . . 4 |- (w = x -> ((-. A.z z = y -> w e. y) <-> (-. A.z z = y -> x e. y)))
7	3, 4, 6	dvelimfALT 1136	. . 3 |- (-. A.z z = x -> ((-. A.z z = y -> x e. y) -> A.z(-. A.z z = y -> x e. y)))
8	1	19.21 1032	. . 3 |- (A.z(-. A.z z = y -> x e. y) <-> (-. A.z z = y -> A.z x e. y))
9	7, 8	syl6ib 212	. 2 |- (-. A.z z = x -> ((-. A.z z = y -> x e. y) -> (-. A.z z = y -> A.z x e. y)))
10	9	pm2.86d 71	1 |- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))

Syntax hints:  -. wn 2   -> wi 3  A.wal 950   = wceq 1099   e. wcel 1105

This theorem is referenced by:  ax11el 1341  axrepnd 4869  axpowndlem4 4875  axregndlem2 4878  axinfndlem1 4880  axinfnd 4881  axacndlem4 4885  axacndlem5 4886  axacnd 4887

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-17 1190

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

Copyright terms: Public domain