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 ⊢∃zz=B
5 4 biantrur ⊢ψ↔∃zz=B∧ψ
6 5 exbii ⊢∃yψ↔∃y∃zz=B∧ψ
7 19.41v ⊢∃zz=B∧ψ↔∃zz=B∧ψ
8 7 exbii ⊢∃y∃zz=B∧ψ↔∃y∃zz=B∧ψ
9 excom ⊢∃y∃zz=B∧ψ↔∃z∃yz=B∧ψ
10 6 8 9 3bitr2i ⊢∃yψ↔∃z∃yz=B∧ψ
11 3 10 bitri ⊢∃xφ↔∃z∃yz=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∀yz=B∧ψ→φ→z=A
24 19.23v ⊢∀yz=B∧ψ→φ→z=A↔∃yz=B∧ψ→φ→z=A
25 24 albii ⊢∀x∀yz=B∧ψ→φ→z=A↔∀x∃yz=B∧ψ→φ→z=A
26 19.21v ⊢∀x∃yz=B∧ψ→φ→z=A↔∃yz=B∧ψ→∀xφ→z=A
27 25 26 bitri ⊢∀x∀yz=B∧ψ→φ→z=A↔∃yz=B∧ψ→∀xφ→z=A
28 23 27 sylib ⊢∀x∀yφ∧ψ→A=B→∃yz=B∧ψ→∀xφ→z=A
29 28 eximdv ⊢∀x∀yφ∧ψ→A=B→∃z∃yz=B∧ψ→∃z∀xφ→z=A
30 11 29 biimtrid ⊢∀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