Theorem eujustALT 2040

Description: A soundness justification theorem for df-eu 2041, showing that the definition is equivalent to itself with its dummy variable renamed. Note that y and z needn't be distinct variables. While this isn't strictly necessary for soundness, the proof provides an example of how it can be achieved through the use of dvelim 2007.

Assertion

Ref	Expression
eujustALT	|- (E.yA.x(ph <-> x = y) <-> E.zA.x(ph <-> x = z))

Distinct variable groups:   x,y   x,z   ph,y   ph,z

Proof of Theorem eujustALT

Step	Hyp	Ref	Expression
1		equequ2 1776	. . . . . 6 |- (y = z -> (x = y <-> x = z))
2	1	bibi2d 753	. . . . 5 |- (y = z -> ((ph <-> x = y) <-> (ph <-> x = z)))
3	2	albidv 1925	. . . 4 |- (y = z -> (A.x(ph <-> x = y) <-> A.x(ph <-> x = z)))
4	3	a4s 1619	. . 3 |- (A.y y = z -> (A.x(ph <-> x = y) <-> A.x(ph <-> x = z)))
5	4	drex1 1797	. 2 |- (A.y y = z -> (E.yA.x(ph <-> x = y) <-> E.zA.x(ph <-> x = z)))
6		hbnae 1788	. . . . . 6 |- (-. A.y y = z -> A.y -. A.y y = z)
7		hbnae 1788	. . . . . 6 |- (-. A.y y = z -> A.z -. A.y y = z)
8	6, 7	19.21ai 1634	. . . . 5 |- (-. A.y y = z -> A.yA.z -. A.y y = z)
9		ax-17 1605	. . . . . . . 8 |- (-. A.x(ph <-> x = w) -> A.z -. A.x(ph <-> x = w))
10		equequ2 1776	. . . . . . . . . . 11 |- (w = y -> (x = w <-> x = y))
11	10	bibi2d 753	. . . . . . . . . 10 |- (w = y -> ((ph <-> x = w) <-> (ph <-> x = y)))
12	11	albidv 1925	. . . . . . . . 9 |- (w = y -> (A.x(ph <-> x = w) <-> A.x(ph <-> x = y)))
13	12	notbid 746	. . . . . . . 8 |- (w = y -> (-. A.x(ph <-> x = w) <-> -. A.x(ph <-> x = y)))
14	9, 13	dvelim 2007	. . . . . . 7 |- (-. A.z z = y -> (-. A.x(ph <-> x = y) -> A.z -. A.x(ph <-> x = y)))
15	14	nalequcoms 1785	. . . . . 6 |- (-. A.y y = z -> (-. A.x(ph <-> x = y) -> A.z -. A.x(ph <-> x = y)))
16		ax-17 1605	. . . . . . 7 |- (-. A.x(ph <-> x = w) -> A.y -. A.x(ph <-> x = w))
17		equequ2 1776	. . . . . . . . . 10 |- (w = z -> (x = w <-> x = z))
18	17	bibi2d 753	. . . . . . . . 9 |- (w = z -> ((ph <-> x = w) <-> (ph <-> x = z)))
19	18	albidv 1925	. . . . . . . 8 |- (w = z -> (A.x(ph <-> x = w) <-> A.x(ph <-> x = z)))
20	19	notbid 746	. . . . . . 7 |- (w = z -> (-. A.x(ph <-> x = w) <-> -. A.x(ph <-> x = z)))
21	16, 20	dvelim 2007	. . . . . 6 |- (-. A.y y = z -> (-. A.x(ph <-> x = z) -> A.y -. A.x(ph <-> x = z)))
22	3	notbid 746	. . . . . . 7 |- (y = z -> (-. A.x(ph <-> x = y) <-> -. A.x(ph <-> x = z)))
23	22	a1i 8	. . . . . 6 |- (-. A.y y = z -> (y = z -> (-. A.x(ph <-> x = y) <-> -. A.x(ph <-> x = z))))
24	15, 21, 23	cbv2 1805	. . . . 5 |- (A.yA.z -. A.y y = z -> (A.y -. A.x(ph <-> x = y) <-> A.z -. A.x(ph <-> x = z)))
25	8, 24	syl 13	. . . 4 |- (-. A.y y = z -> (A.y -. A.x(ph <-> x = y) <-> A.z -. A.x(ph <-> x = z)))
26	25	notbid 746	. . 3 |- (-. A.y y = z -> (-. A.y -. A.x(ph <-> x = y) <-> -. A.z -. A.x(ph <-> x = z)))
27		df-ex 1616	. . 3 |- (E.yA.x(ph <-> x = y) <-> -. A.y -. A.x(ph <-> x = y))
28		df-ex 1616	. . 3 |- (E.zA.x(ph <-> x = z) <-> -. A.z -. A.x(ph <-> x = z))
29	26, 27, 28	3bitr4g 745	. 2 |- (-. A.y y = z -> (E.yA.x(ph <-> x = y) <-> E.zA.x(ph <-> x = z)))
30	5, 29	pm2.61i 192	1 |- (E.yA.x(ph <-> x = y) <-> E.zA.x(ph <-> x = z))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219  A.wal 1584   = wceq 1586  E.wex 1615

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-10 1596  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-11o 1864

This theorem depends on definitions:  df-bi 220  df-an 339  df-ex 1616  df-sb 1816

Copyright terms: Public domain