Theorem 2eu8 1455

Description: Two equivalent expressions for double existential uniqueness. Curiously, we can put ∃! on either of the internal conjuncts but not both. We can also commute ∃!x∃!y using 2eu7 1454.

Assertion

Ref	Expression
2eu8	⊢ (∃!x∃!y(∃xφ ⋀ ∃yφ) ↔ ∃!x∃!y(∃!xφ ⋀ ∃yφ))

Proof of Theorem 2eu8

Step	Hyp	Ref	Expression
1		2eu2 1449	. . 3 ⊢ (∃!x∃yφ → (∃!y∃!xφ ↔ ∃!y∃xφ))
2	1	pm5.32i 644	. 2 ⊢ ((∃!x∃yφ ⋀ ∃!y∃!xφ) ↔ (∃!x∃yφ ⋀ ∃!y∃xφ))
3		hbeu1 1387	. . . . 5 ⊢ (∃!xφ → ∀x∃!xφ)
4	3	hbeu 1388	. . . 4 ⊢ (∃!y∃!xφ → ∀x∃!y∃!xφ)
5	4	euan 1427	. . 3 ⊢ (∃!x(∃!y∃!xφ ⋀ ∃yφ) ↔ (∃!y∃!xφ ⋀ ∃!x∃yφ))
6		ancom 435	. . . . . 6 ⊢ ((∃!xφ ⋀ ∃yφ) ↔ (∃yφ ⋀ ∃!xφ))
7	6	eubii 1386	. . . . 5 ⊢ (∃!y(∃!xφ ⋀ ∃yφ) ↔ ∃!y(∃yφ ⋀ ∃!xφ))
8		hbe1 1015	. . . . . 6 ⊢ (∃yφ → ∀y∃yφ)
9	8	euan 1427	. . . . 5 ⊢ (∃!y(∃yφ ⋀ ∃!xφ) ↔ (∃yφ ⋀ ∃!y∃!xφ))
10		ancom 435	. . . . 5 ⊢ ((∃yφ ⋀ ∃!y∃!xφ) ↔ (∃!y∃!xφ ⋀ ∃yφ))
11	7, 9, 10	3bitr 177	. . . 4 ⊢ (∃!y(∃!xφ ⋀ ∃yφ) ↔ (∃!y∃!xφ ⋀ ∃yφ))
12	11	eubii 1386	. . 3 ⊢ (∃!x∃!y(∃!xφ ⋀ ∃yφ) ↔ ∃!x(∃!y∃!xφ ⋀ ∃yφ))
13		ancom 435	. . 3 ⊢ ((∃!x∃yφ ⋀ ∃!y∃!xφ) ↔ (∃!y∃!xφ ⋀ ∃!x∃yφ))
14	5, 12, 13	3bitr4r 184	. 2 ⊢ ((∃!x∃yφ ⋀ ∃!y∃!xφ) ↔ ∃!x∃!y(∃!xφ ⋀ ∃yφ))
15		2eu7 1454	. 2 ⊢ ((∃!x∃yφ ⋀ ∃!y∃xφ) ↔ ∃!x∃!y(∃xφ ⋀ ∃yφ))
16	2, 14, 15	3bitr3r 182	1 ⊢ (∃!x∃!y(∃xφ ⋀ ∃yφ) ↔ ∃!x∃!y(∃!xφ ⋀ ∃yφ))

Syntax hints:   ↔ wb 146   ⋀ wa 223  ∃wex 979  ∃!weu 1379

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382

Copyright terms: Public domain