Theorem ax15 1359

Description: Axiom ax-15 1360 is redundant if we assume ax-17 971. 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 1357 and ax-17 971. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements.

This theorem should not be referenced in any proof. Instead, use ax-15 1360 below so that theorems needing ax-15 1360 can be more easily identified.

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 1015	. . . . 5 |- (-. A.z z = y -> A.z -. A.z z = y)
2		dveel2 1357	. . . . 5 |- (-. A.z z = y -> (w e. y -> A.z w e. y))
3	1, 2	hbim1 1103	. . . 4 |- ((-. A.z z = y -> w e. y) -> A.z(-. A.z z = y -> w e. y))
4		ax-17 971	. . . 4 |- ((-. A.z z = y -> x e. y) -> A.w(-. A.z z = y -> x e. y))
5		elequ1 1136	. . . . 5 |- (w = x -> (w e. y <-> x e. y))
6	5	imbi2d 612	. . . 4 |- (w = x -> ((-. A.z z = y -> w e. y) <-> (-. A.z z = y -> x e. y)))
7	3, 4, 6	dvelimfALT 1153	. . 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 1056	. . 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 954   = wceq 956   e. wcel 958

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-13 969  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