Metamath Proof Explorer

Theorem reuind

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

Ref Expression
Hypotheses reuind.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
reuind.2 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
Assertion reuind ( ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → 𝐴 = 𝐵 ) ∧ ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ) → ∃! 𝑧 ∈ 𝐶 ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 reuind.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 reuind.2 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
3 2 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶 ) )
4 3 1 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ↔ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) )
5 4 cbvexvw ⊢ ( ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) )
6 r19.41v ⊢ ( ∃ 𝑧 ∈ 𝐶 ( 𝑧 = 𝐵 ∧ 𝜓 ) ↔ ( ∃ 𝑧 ∈ 𝐶 𝑧 = 𝐵 ∧ 𝜓 ) )
7 6 exbii ⊢ ( ∃ 𝑦 ∃ 𝑧 ∈ 𝐶 ( 𝑧 = 𝐵 ∧ 𝜓 ) ↔ ∃ 𝑦 ( ∃ 𝑧 ∈ 𝐶 𝑧 = 𝐵 ∧ 𝜓 ) )
8 rexcom4 ⊢ ( ∃ 𝑧 ∈ 𝐶 ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) ↔ ∃ 𝑦 ∃ 𝑧 ∈ 𝐶 ( 𝑧 = 𝐵 ∧ 𝜓 ) )
9 risset ⊢ ( 𝐵 ∈ 𝐶 ↔ ∃ 𝑧 ∈ 𝐶 𝑧 = 𝐵 )
10 9 anbi1i ⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ↔ ( ∃ 𝑧 ∈ 𝐶 𝑧 = 𝐵 ∧ 𝜓 ) )
11 10 exbii ⊢ ( ∃ 𝑦 ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ↔ ∃ 𝑦 ( ∃ 𝑧 ∈ 𝐶 𝑧 = 𝐵 ∧ 𝜓 ) )
12 7 8 11 3bitr4ri ⊢ ( ∃ 𝑦 ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ↔ ∃ 𝑧 ∈ 𝐶 ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) )
13 5 12 bitri ⊢ ( ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ↔ ∃ 𝑧 ∈ 𝐶 ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) )
14 eqeq2 ⊢ ( 𝐴 = 𝐵 → ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) )
15 14 imim2i ⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → 𝐴 = 𝐵 ) → ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) )
16 biimpr ⊢ ( ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) → ( 𝑧 = 𝐵 → 𝑧 = 𝐴 ) )
17 16 imim2i ⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) → ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( 𝑧 = 𝐵 → 𝑧 = 𝐴 ) ) )
18 an31 ⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) ∧ 𝑧 = 𝐵 ) ↔ ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ) )
19 18 imbi1i ⊢ ( ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐴 ) ↔ ( ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ) → 𝑧 = 𝐴 ) )
20 impexp ⊢ ( ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐴 ) ↔ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( 𝑧 = 𝐵 → 𝑧 = 𝐴 ) ) )
21 impexp ⊢ ( ( ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ) → 𝑧 = 𝐴 ) ↔ ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
22 19 20 21 3bitr3i ⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( 𝑧 = 𝐵 → 𝑧 = 𝐴 ) ) ↔ ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
23 17 22 sylib ⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) → ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
24 15 23 syl ⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → 𝐴 = 𝐵 ) → ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
25 24 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → 𝐴 = 𝐵 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
26 19.23v ⊢ ( ∀ 𝑦 ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) ↔ ( ∃ 𝑦 ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
27 an12 ⊢ ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) ↔ ( 𝐵 ∈ 𝐶 ∧ ( 𝑧 = 𝐵 ∧ 𝜓 ) ) )
28 eleq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶 ) )
29 28 adantr ⊢ ( ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶 ) )
30 29 pm5.32ri ⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑧 = 𝐵 ∧ 𝜓 ) ) ↔ ( 𝐵 ∈ 𝐶 ∧ ( 𝑧 = 𝐵 ∧ 𝜓 ) ) )
31 27 30 bitr4i ⊢ ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) ↔ ( 𝑧 ∈ 𝐶 ∧ ( 𝑧 = 𝐵 ∧ 𝜓 ) ) )
32 31 exbii ⊢ ( ∃ 𝑦 ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝐶 ∧ ( 𝑧 = 𝐵 ∧ 𝜓 ) ) )
33 19.42v ⊢ ( ∃ 𝑦 ( 𝑧 ∈ 𝐶 ∧ ( 𝑧 = 𝐵 ∧ 𝜓 ) ) ↔ ( 𝑧 ∈ 𝐶 ∧ ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) ) )
34 32 33 bitri ⊢ ( ∃ 𝑦 ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) ↔ ( 𝑧 ∈ 𝐶 ∧ ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) ) )
35 34 imbi1i ⊢ ( ( ∃ 𝑦 ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) ↔ ( ( 𝑧 ∈ 𝐶 ∧ ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
36 26 35 bitri ⊢ ( ∀ 𝑦 ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) ↔ ( ( 𝑧 ∈ 𝐶 ∧ ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
37 36 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) ↔ ∀ 𝑥 ( ( 𝑧 ∈ 𝐶 ∧ ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
38 19.21v ⊢ ( ∀ 𝑥 ( ( 𝑧 ∈ 𝐶 ∧ ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) ↔ ( ( 𝑧 ∈ 𝐶 ∧ ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) ) → ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
39 37 38 bitri ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑧 = 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) ↔ ( ( 𝑧 ∈ 𝐶 ∧ ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) ) → ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
40 25 39 sylib ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → 𝐴 = 𝐵 ) → ( ( 𝑧 ∈ 𝐶 ∧ ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) ) → ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
41 40 expd ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → 𝐴 = 𝐵 ) → ( 𝑧 ∈ 𝐶 → ( ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) → ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) ) )
42 41 reximdvai ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → 𝐴 = 𝐵 ) → ( ∃ 𝑧 ∈ 𝐶 ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) → ∃ 𝑧 ∈ 𝐶 ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
43 13 42 biimtrid ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → 𝐴 = 𝐵 ) → ( ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → ∃ 𝑧 ∈ 𝐶 ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ) )
44 43 imp ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → 𝐴 = 𝐵 ) ∧ ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ) → ∃ 𝑧 ∈ 𝐶 ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) )
45 pm4.24 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ↔ ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ) )
46 45 biimpi ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ) )
47 anim12 ⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ∧ ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑤 = 𝐴 ) ) → ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ) → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐴 ) ) )
48 eqtr3 ⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐴 ) → 𝑧 = 𝑤 )
49 46 47 48 syl56 ⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ∧ ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑤 = 𝐴 ) ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝑤 ) )
50 49 alanimi ⊢ ( ( ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑤 = 𝐴 ) ) → ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝑤 ) )
51 19.23v ⊢ ( ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝑤 ) ↔ ( ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝑤 ) )
52 50 51 sylib ⊢ ( ( ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑤 = 𝐴 ) ) → ( ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝑤 ) )
53 52 com12 ⊢ ( ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → ( ( ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑤 = 𝐴 ) ) → 𝑧 = 𝑤 ) )
54 53 a1d ⊢ ( ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶 ) → ( ( ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑤 = 𝐴 ) ) → 𝑧 = 𝑤 ) ) )
55 54 ralrimivv ⊢ ( ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → ∀ 𝑧 ∈ 𝐶 ∀ 𝑤 ∈ 𝐶 ( ( ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑤 = 𝐴 ) ) → 𝑧 = 𝑤 ) )
56 55 adantl ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → 𝐴 = 𝐵 ) ∧ ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ) → ∀ 𝑧 ∈ 𝐶 ∀ 𝑤 ∈ 𝐶 ( ( ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑤 = 𝐴 ) ) → 𝑧 = 𝑤 ) )
57 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = 𝐴 ↔ 𝑤 = 𝐴 ) )
58 57 imbi2d ⊢ ( 𝑧 = 𝑤 → ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ↔ ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑤 = 𝐴 ) ) )
59 58 albidv ⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ↔ ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑤 = 𝐴 ) ) )
60 59 reu4 ⊢ ( ∃! 𝑧 ∈ 𝐶 ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ↔ ( ∃ 𝑧 ∈ 𝐶 ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐶 ∀ 𝑤 ∈ 𝐶 ( ( ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑤 = 𝐴 ) ) → 𝑧 = 𝑤 ) ) )
61 44 56 60 sylanbrc ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ∧ ( 𝐵 ∈ 𝐶 ∧ 𝜓 ) ) → 𝐴 = 𝐵 ) ∧ ∃ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) ) → ∃! 𝑧 ∈ 𝐶 ∀ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝜑 ) → 𝑧 = 𝐴 ) )