Theorem ax15 1352

Description: Axiom ax-15 1353 is redundant if we assume ax-17 968. 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 1350 and ax-17 968. 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 1353 below so that theorems needing ax-15 1353 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 1011	. . . . 5 |- (-. A.z z = y -> A.z -. A.z z = y)
2		dveel2 1350	. . . . 5 |- (-. A.z z = y -> (w e. y -> A.z w e. y))
3	1, 2	hbim1 1099	. . . 4 |- ((-. A.z z = y -> w e. y) -> A.z(-. A.z z = y -> w e. y))
4		ax-17 968	. . . 4 |- ((-. A.z z = y -> x e. y) -> A.w(-. A.z z = y -> x e. y))
5		elequ1 1132	. . . . 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 1149	. . 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 1052	. . 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 951   = wceq 953   e. wcel 955

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136

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

Copyright terms: Public domain