Theorem ax15 2021

Description: Axiom ax-15 2143 is redundant if we assume ax-17 1616. 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 2020 and ax-17 1616. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements. (Contributed by NM, 29-Jun-1995.) (Proof modification is discouraged.)

Assertion

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

Proof of Theorem ax15

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hbn1 1730	. . . . 5 |- (-. A.z z = y -> A.z -. A.z z = y)
2		dveel2 2020	. . . . 5 |- (-. A.z z = y -> (w e. y -> A.z w e. y))
3	1, 2	hbim1 1810	. . . 4 |- ((-. A.z z = y -> w e. y) -> A.z(-. A.z z = y -> w e. y))
4		elequ1 1713	. . . . 5 |- (w = x -> (w e. y <-> x e. y))
5	4	imbi2d 307	. . . 4 |- (w = x -> ((-. A.z z = y -> w e. y) <-> (-. A.z z = y -> x e. y)))
6	3, 5	dvelim 2016	. . 3 |- (-. A.z z = x -> ((-. A.z z = y -> x e. y) -> A.z(-. A.z z = y -> x e. y)))
7		nfa1 1788	. . . . 5 |- F/zA.z z = y
8	7	nfn 1793	. . . 4 |- F/z -. A.z z = y
9	8	19.21 1796	. . 3 |- (A.z(-. A.z z = y -> x e. y) <-> (-. A.z z = y -> A.z x e. y))
10	6, 9	syl6ib 217	. 2 |- (-. A.z z = x -> ((-. A.z z = y -> x e. y) -> (-. A.z z = y -> A.z x e. y)))
11	10	pm2.86d 93	1 |- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))

Syntax hints:  -. wn 3   -> wi 4  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by: (None)