Theorem eujustALT 2207

Description: A soundness justification theorem for df-eu 2208, 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 2016. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Allowed substitution hint:   ph(x)

Proof of Theorem eujustALT

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		equequ2 1686	. . . . . 6 |- (y = z -> (x = y <-> x = z))
2	1	bibi2d 309	. . . . 5 |- (y = z -> ((ph <-> x = y) <-> (ph <-> x = z)))
3	2	albidv 1625	. . . 4 |- (y = z -> (A.x(ph <-> x = y) <-> A.x(ph <-> x = z)))
4	3	sps 1754	. . 3 |- (A.y y = z -> (A.x(ph <-> x = y) <-> A.x(ph <-> x = z)))
5	4	drex1 1967	. 2 |- (A.y y = z -> (E.yA.x(ph <-> x = y) <-> E.zA.x(ph <-> x = z)))
6		hbnae 1955	. . . . . 6 |- (-. A.y y = z -> A.y -. A.y y = z)
7		hbnae 1955	. . . . . 6 |- (-. A.y y = z -> A.z -. A.y y = z)
8	6, 7	alrimih 1565	. . . . 5 |- (-. A.y y = z -> A.yA.z -. A.y y = z)
9		ax-17 1616	. . . . . . . 8 |- (-. A.x(ph <-> x = w) -> A.z -. A.x(ph <-> x = w))
10		equequ2 1686	. . . . . . . . . . 11 |- (w = y -> (x = w <-> x = y))
11	10	bibi2d 309	. . . . . . . . . 10 |- (w = y -> ((ph <-> x = w) <-> (ph <-> x = y)))
12	11	albidv 1625	. . . . . . . . 9 |- (w = y -> (A.x(ph <-> x = w) <-> A.x(ph <-> x = y)))
13	12	notbid 285	. . . . . . . 8 |- (w = y -> (-. A.x(ph <-> x = w) <-> -. A.x(ph <-> x = y)))
14	9, 13	dvelim 2016	. . . . . . 7 |- (-. A.z z = y -> (-. A.x(ph <-> x = y) -> A.z -. A.x(ph <-> x = y)))
15	14	naecoms 1948	. . . . . 6 |- (-. A.y y = z -> (-. A.x(ph <-> x = y) -> A.z -. A.x(ph <-> x = y)))
16		ax-17 1616	. . . . . . 7 |- (-. A.x(ph <-> x = w) -> A.y -. A.x(ph <-> x = w))
17		equequ2 1686	. . . . . . . . . 10 |- (w = z -> (x = w <-> x = z))
18	17	bibi2d 309	. . . . . . . . 9 |- (w = z -> ((ph <-> x = w) <-> (ph <-> x = z)))
19	18	albidv 1625	. . . . . . . 8 |- (w = z -> (A.x(ph <-> x = w) <-> A.x(ph <-> x = z)))
20	19	notbid 285	. . . . . . 7 |- (w = z -> (-. A.x(ph <-> x = w) <-> -. A.x(ph <-> x = z)))
21	16, 20	dvelim 2016	. . . . . 6 |- (-. A.y y = z -> (-. A.x(ph <-> x = z) -> A.y -. A.x(ph <-> x = z)))
22	3	notbid 285	. . . . . . 7 |- (y = z -> (-. A.x(ph <-> x = y) <-> -. A.x(ph <-> x = z)))
23	22	a1i 10	. . . . . 6 |- (-. A.y y = z -> (y = z -> (-. A.x(ph <-> x = y) <-> -. A.x(ph <-> x = z))))
24	15, 21, 23	cbv2h 1980	. . . . 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 15	. . . 4 |- (-. A.y y = z -> (A.y -. A.x(ph <-> x = y) <-> A.z -. A.x(ph <-> x = z)))
26	25	notbid 285	. . 3 |- (-. A.y y = z -> (-. A.y -. A.x(ph <-> x = y) <-> -. A.z -. A.x(ph <-> x = z)))
27		df-ex 1542	. . 3 |- (E.yA.x(ph <-> x = y) <-> -. A.y -. A.x(ph <-> x = y))
28		df-ex 1542	. . 3 |- (E.zA.x(ph <-> x = z) <-> -. A.z -. A.x(ph <-> x = z))
29	26, 27, 28	3bitr4g 279	. 2 |- (-. A.y y = z -> (E.yA.x(ph <-> x = y) <-> E.zA.x(ph <-> x = z)))
30	5, 29	pm2.61i 156	1 |- (E.yA.x(ph <-> x = y) <-> E.zA.x(ph <-> x = z))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176  A.wal 1540  E.wex 1541

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-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)