Metamath Proof Explorer

Theorem euind

Description: Existential uniqueness via an indirect equality. (Contributed by NM, 11-Oct-2010)

Ref Expression
Hypotheses euind.1 ⊢ B ∈ V
euind.2 ⊢ x = y → φ ↔ ψ
Assertion euind ⊢ ∀ x ∀ y φ ∧ ψ → A = B ∧ ∃ x φ → ∃! z ∀ x φ → z = A

Proof

Step Hyp Ref Expression
1 euind.1 ⊢ B ∈ V
2 euind.2 ⊢ x = y → φ ↔ ψ
3 2 cbvexvw ⊢ ∃ x φ ↔ ∃ y ψ
4 1 isseti ⊢ ∃ z z = B
5 4 biantrur ⊢ ψ ↔ ∃ z z = B ∧ ψ
6 5 exbii ⊢ ∃ y ψ ↔ ∃ y ∃ z z = B ∧ ψ
7 19.41v ⊢ ∃ z z = B ∧ ψ ↔ ∃ z z = B ∧ ψ
8 7 exbii ⊢ ∃ y ∃ z z = B ∧ ψ ↔ ∃ y ∃ z z = B ∧ ψ
9 excom ⊢ ∃ y ∃ z z = B ∧ ψ ↔ ∃ z ∃ y z = B ∧ ψ
10 6 8 9 3bitr2i ⊢ ∃ y ψ ↔ ∃ z ∃ y z = B ∧ ψ
11 3 10 bitri ⊢ ∃ x φ ↔ ∃ z ∃ y z = B ∧ ψ
12 eqeq2 ⊢ A = B → z = A ↔ z = B
13 12 imim2i ⊢ φ ∧ ψ → A = B → φ ∧ ψ → z = A ↔ z = B
14 biimpr ⊢ z = A ↔ z = B → z = B → z = A
15 14 imim2i ⊢ φ ∧ ψ → z = A ↔ z = B → φ ∧ ψ → z = B → z = A
16 an31 ⊢ φ ∧ ψ ∧ z = B ↔ z = B ∧ ψ ∧ φ
17 16 imbi1i ⊢ φ ∧ ψ ∧ z = B → z = A ↔ z = B ∧ ψ ∧ φ → z = A
18 impexp ⊢ φ ∧ ψ ∧ z = B → z = A ↔ φ ∧ ψ → z = B → z = A
19 impexp ⊢ z = B ∧ ψ ∧ φ → z = A ↔ z = B ∧ ψ → φ → z = A
20 17 18 19 3bitr3i ⊢ φ ∧ ψ → z = B → z = A ↔ z = B ∧ ψ → φ → z = A
21 15 20 sylib ⊢ φ ∧ ψ → z = A ↔ z = B → z = B ∧ ψ → φ → z = A
22 13 21 syl ⊢ φ ∧ ψ → A = B → z = B ∧ ψ → φ → z = A
23 22 2alimi ⊢ ∀ x ∀ y φ ∧ ψ → A = B → ∀ x ∀ y z = B ∧ ψ → φ → z = A
24 19.23v ⊢ ∀ y z = B ∧ ψ → φ → z = A ↔ ∃ y z = B ∧ ψ → φ → z = A
25 24 albii ⊢ ∀ x ∀ y z = B ∧ ψ → φ → z = A ↔ ∀ x ∃ y z = B ∧ ψ → φ → z = A
26 19.21v ⊢ ∀ x ∃ y z = B ∧ ψ → φ → z = A ↔ ∃ y z = B ∧ ψ → ∀ x φ → z = A
27 25 26 bitri ⊢ ∀ x ∀ y z = B ∧ ψ → φ → z = A ↔ ∃ y z = B ∧ ψ → ∀ x φ → z = A
28 23 27 sylib ⊢ ∀ x ∀ y φ ∧ ψ → A = B → ∃ y z = B ∧ ψ → ∀ x φ → z = A
29 28 eximdv ⊢ ∀ x ∀ y φ ∧ ψ → A = B → ∃ z ∃ y z = B ∧ ψ → ∃ z ∀ x φ → z = A
30 11 29 syl5bi ⊢ ∀ x ∀ y φ ∧ ψ → A = B → ∃ x φ → ∃ z ∀ x φ → z = A
31 30 imp ⊢ ∀ x ∀ y φ ∧ ψ → A = B ∧ ∃ x φ → ∃ z ∀ x φ → z = A
32 pm4.24 ⊢ φ ↔ φ ∧ φ
33 32 biimpi ⊢ φ → φ ∧ φ
34 anim12 ⊢ φ → z = A ∧ φ → w = A → φ ∧ φ → z = A ∧ w = A
35 eqtr3 ⊢ z = A ∧ w = A → z = w
36 33 34 35 syl56 ⊢ φ → z = A ∧ φ → w = A → φ → z = w
37 36 alanimi ⊢ ∀ x φ → z = A ∧ ∀ x φ → w = A → ∀ x φ → z = w
38 19.23v ⊢ ∀ x φ → z = w ↔ ∃ x φ → z = w
39 37 38 sylib ⊢ ∀ x φ → z = A ∧ ∀ x φ → w = A → ∃ x φ → z = w
40 39 com12 ⊢ ∃ x φ → ∀ x φ → z = A ∧ ∀ x φ → w = A → z = w
41 40 alrimivv ⊢ ∃ x φ → ∀ z ∀ w ∀ x φ → z = A ∧ ∀ x φ → w = A → z = w
42 41 adantl ⊢ ∀ x ∀ y φ ∧ ψ → A = B ∧ ∃ x φ → ∀ z ∀ w ∀ x φ → z = A ∧ ∀ x φ → w = A → z = w
43 eqeq1 ⊢ z = w → z = A ↔ w = A
44 43 imbi2d ⊢ z = w → φ → z = A ↔ φ → w = A
45 44 albidv ⊢ z = w → ∀ x φ → z = A ↔ ∀ x φ → w = A
46 45 eu4 ⊢ ∃! z ∀ x φ → z = A ↔ ∃ z ∀ x φ → z = A ∧ ∀ z ∀ w ∀ x φ → z = A ∧ ∀ x φ → w = A → z = w
47 31 42 46 sylanbrc ⊢ ∀ x ∀ y φ ∧ ψ → A = B ∧ ∃ x φ → ∃! z ∀ x φ → z = A