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	⊢ (∃y∀x(φ ↔ x = y) ↔ ∃z∀x(φ ↔ x = z))

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

Allowed substitution hint:   φ(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 → ((φ ↔ x = y) ↔ (φ ↔ x = z)))
3	2	albidv 1625	. . . 4 ⊢ (y = z → (∀x(φ ↔ x = y) ↔ ∀x(φ ↔ x = z)))
4	3	sps 1754	. . 3 ⊢ (∀y y = z → (∀x(φ ↔ x = y) ↔ ∀x(φ ↔ x = z)))
5	4	drex1 1967	. 2 ⊢ (∀y y = z → (∃y∀x(φ ↔ x = y) ↔ ∃z∀x(φ ↔ x = z)))
6		hbnae 1955	. . . . . 6 ⊢ (¬ ∀y y = z → ∀y ¬ ∀y y = z)
7		hbnae 1955	. . . . . 6 ⊢ (¬ ∀y y = z → ∀z ¬ ∀y y = z)
8	6, 7	alrimih 1565	. . . . 5 ⊢ (¬ ∀y y = z → ∀y∀z ¬ ∀y y = z)
9		ax-17 1616	. . . . . . . 8 ⊢ (¬ ∀x(φ ↔ x = w) → ∀z ¬ ∀x(φ ↔ x = w))
10		equequ2 1686	. . . . . . . . . . 11 ⊢ (w = y → (x = w ↔ x = y))
11	10	bibi2d 309	. . . . . . . . . 10 ⊢ (w = y → ((φ ↔ x = w) ↔ (φ ↔ x = y)))
12	11	albidv 1625	. . . . . . . . 9 ⊢ (w = y → (∀x(φ ↔ x = w) ↔ ∀x(φ ↔ x = y)))
13	12	notbid 285	. . . . . . . 8 ⊢ (w = y → (¬ ∀x(φ ↔ x = w) ↔ ¬ ∀x(φ ↔ x = y)))
14	9, 13	dvelim 2016	. . . . . . 7 ⊢ (¬ ∀z z = y → (¬ ∀x(φ ↔ x = y) → ∀z ¬ ∀x(φ ↔ x = y)))
15	14	naecoms 1948	. . . . . 6 ⊢ (¬ ∀y y = z → (¬ ∀x(φ ↔ x = y) → ∀z ¬ ∀x(φ ↔ x = y)))
16		ax-17 1616	. . . . . . 7 ⊢ (¬ ∀x(φ ↔ x = w) → ∀y ¬ ∀x(φ ↔ x = w))
17		equequ2 1686	. . . . . . . . . 10 ⊢ (w = z → (x = w ↔ x = z))
18	17	bibi2d 309	. . . . . . . . 9 ⊢ (w = z → ((φ ↔ x = w) ↔ (φ ↔ x = z)))
19	18	albidv 1625	. . . . . . . 8 ⊢ (w = z → (∀x(φ ↔ x = w) ↔ ∀x(φ ↔ x = z)))
20	19	notbid 285	. . . . . . 7 ⊢ (w = z → (¬ ∀x(φ ↔ x = w) ↔ ¬ ∀x(φ ↔ x = z)))
21	16, 20	dvelim 2016	. . . . . 6 ⊢ (¬ ∀y y = z → (¬ ∀x(φ ↔ x = z) → ∀y ¬ ∀x(φ ↔ x = z)))
22	3	notbid 285	. . . . . . 7 ⊢ (y = z → (¬ ∀x(φ ↔ x = y) ↔ ¬ ∀x(φ ↔ x = z)))
23	22	a1i 10	. . . . . 6 ⊢ (¬ ∀y y = z → (y = z → (¬ ∀x(φ ↔ x = y) ↔ ¬ ∀x(φ ↔ x = z))))
24	15, 21, 23	cbv2h 1980	. . . . 5 ⊢ (∀y∀z ¬ ∀y y = z → (∀y ¬ ∀x(φ ↔ x = y) ↔ ∀z ¬ ∀x(φ ↔ x = z)))
25	8, 24	syl 15	. . . 4 ⊢ (¬ ∀y y = z → (∀y ¬ ∀x(φ ↔ x = y) ↔ ∀z ¬ ∀x(φ ↔ x = z)))
26	25	notbid 285	. . 3 ⊢ (¬ ∀y y = z → (¬ ∀y ¬ ∀x(φ ↔ x = y) ↔ ¬ ∀z ¬ ∀x(φ ↔ x = z)))
27		df-ex 1542	. . 3 ⊢ (∃y∀x(φ ↔ x = y) ↔ ¬ ∀y ¬ ∀x(φ ↔ x = y))
28		df-ex 1542	. . 3 ⊢ (∃z∀x(φ ↔ x = z) ↔ ¬ ∀z ¬ ∀x(φ ↔ x = z))
29	26, 27, 28	3bitr4g 279	. 2 ⊢ (¬ ∀y y = z → (∃y∀x(φ ↔ x = y) ↔ ∃z∀x(φ ↔ x = z)))
30	5, 29	pm2.61i 156	1 ⊢ (∃y∀x(φ ↔ x = y) ↔ ∃z∀x(φ ↔ x = z))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176  ∀wal 1540  ∃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)