Metamath Proof Explorer

Theorem eu6w

Description: Replace ax-10 , ax-12 in eu6 with substitution hypotheses. (Contributed by SN, 27-May-2025)

Ref Expression
Hypotheses eu6w.x ⊢ x = z → φ ↔ ψ
eu6w.y ⊢ x = y → φ ↔ θ
Assertion eu6w ⊢ ∃! x φ ↔ ∃ y ∀ x φ ↔ x = y

Proof

Step Hyp Ref Expression
1 eu6w.x ⊢ x = z → φ ↔ ψ
2 eu6w.y ⊢ x = y → φ ↔ θ
3 alnex ⊢ ∀ x ¬ φ ↔ ¬ ∃ x φ
4 pm2.21 ⊢ ¬ φ → φ → x = y
5 4 alimi ⊢ ∀ x ¬ φ → ∀ x φ → x = y
6 3 5 sylbir ⊢ ¬ ∃ x φ → ∀ x φ → x = y
7 equequ2 ⊢ y = z → x = y ↔ x = z
8 7 imbi2d ⊢ y = z → φ → x = y ↔ φ → x = z
9 8 albidv ⊢ y = z → ∀ x φ → x = y ↔ ∀ x φ → x = z
10 9 19.8aw ⊢ ∀ x φ → x = y → ∃ y ∀ x φ → x = y
11 6 10 syl ⊢ ¬ ∃ x φ → ∃ y ∀ x φ → x = y
12 biimp ⊢ φ ↔ x = y → φ → x = y
13 12 alimi ⊢ ∀ x φ ↔ x = y → ∀ x φ → x = y
14 13 eximi ⊢ ∃ y ∀ x φ ↔ x = y → ∃ y ∀ x φ → x = y
15 11 14 ja ⊢ ∃ x φ → ∃ y ∀ x φ ↔ x = y → ∃ y ∀ x φ → x = y
16 equequ1 ⊢ x = z → x = y ↔ z = y
17 1 16 imbi12d ⊢ x = z → φ → x = y ↔ ψ → z = y
18 17 nfa1w ⊢ Ⅎ x ∀ x φ → x = y
19 1 16 bibi12d ⊢ x = z → φ ↔ x = y ↔ ψ ↔ z = y
20 19 nfa1w ⊢ Ⅎ x ∀ x φ ↔ x = y
21 18 20 nfim ⊢ Ⅎ x ∀ x φ → x = y → ∀ x φ ↔ x = y
22 19.38b ⊢ Ⅎ x ∀ x φ → x = y → ∀ x φ ↔ x = y → ∃ x φ → ∀ x ∀ x φ → x = y → ∀ x φ ↔ x = y ↔ ∀ x φ → ∀ x φ → x = y → ∀ x φ ↔ x = y
23 17 cbvalvw ⊢ ∀ x φ → x = y ↔ ∀ z ψ → z = y
24 19 cbvalvw ⊢ ∀ x φ ↔ x = y ↔ ∀ z ψ ↔ z = y
25 23 24 imbi12i ⊢ ∀ x φ → x = y → ∀ x φ ↔ x = y ↔ ∀ z ψ → z = y → ∀ z ψ ↔ z = y
26 25 a1i ⊢ x = z → ∀ x φ → x = y → ∀ x φ ↔ x = y ↔ ∀ z ψ → z = y → ∀ z ψ ↔ z = y
27 26 spw ⊢ ∀ x ∀ x φ → x = y → ∀ x φ ↔ x = y → ∀ x φ → x = y → ∀ x φ ↔ x = y
28 26 19.8aw ⊢ ∀ x φ → x = y → ∀ x φ ↔ x = y → ∃ x ∀ x φ → x = y → ∀ x φ ↔ x = y
29 id ⊢ Ⅎ x ∀ x φ → x = y → ∀ x φ ↔ x = y → Ⅎ x ∀ x φ → x = y → ∀ x φ ↔ x = y
30 29 nfrd ⊢ Ⅎ x ∀ x φ → x = y → ∀ x φ ↔ x = y → ∃ x ∀ x φ → x = y → ∀ x φ ↔ x = y → ∀ x ∀ x φ → x = y → ∀ x φ ↔ x = y
31 28 30 syl5 ⊢ Ⅎ x ∀ x φ → x = y → ∀ x φ ↔ x = y → ∀ x φ → x = y → ∀ x φ ↔ x = y → ∀ x ∀ x φ → x = y → ∀ x φ ↔ x = y
32 27 31 impbid2 ⊢ Ⅎ x ∀ x φ → x = y → ∀ x φ ↔ x = y → ∀ x ∀ x φ → x = y → ∀ x φ ↔ x = y ↔ ∀ x φ → x = y → ∀ x φ ↔ x = y
33 32 imbi2d ⊢ Ⅎ x ∀ x φ → x = y → ∀ x φ ↔ x = y → ∃ x φ → ∀ x ∀ x φ → x = y → ∀ x φ ↔ x = y ↔ ∃ x φ → ∀ x φ → x = y → ∀ x φ ↔ x = y
34 22 33 bitr3d ⊢ Ⅎ x ∀ x φ → x = y → ∀ x φ ↔ x = y → ∀ x φ → ∀ x φ → x = y → ∀ x φ ↔ x = y ↔ ∃ x φ → ∀ x φ → x = y → ∀ x φ ↔ x = y
35 21 34 ax-mp ⊢ ∀ x φ → ∀ x φ → x = y → ∀ x φ ↔ x = y ↔ ∃ x φ → ∀ x φ → x = y → ∀ x φ ↔ x = y
36 17 spw ⊢ ∀ x φ → x = y → φ → x = y
37 id ⊢ φ → φ
38 2 ax12wlem ⊢ x = y → φ → ∀ x x = y → φ
39 38 com12 ⊢ φ → x = y → ∀ x x = y → φ
40 37 39 embantd ⊢ φ → φ → x = y → ∀ x x = y → φ
41 36 40 syl5 ⊢ φ → ∀ x φ → x = y → ∀ x x = y → φ
42 41 ancld ⊢ φ → ∀ x φ → x = y → ∀ x φ → x = y ∧ ∀ x x = y → φ
43 albiim ⊢ ∀ x φ ↔ x = y ↔ ∀ x φ → x = y ∧ ∀ x x = y → φ
44 42 43 imbitrrdi ⊢ φ → ∀ x φ → x = y → ∀ x φ ↔ x = y
45 35 44 mpgbi ⊢ ∃ x φ → ∀ x φ → x = y → ∀ x φ ↔ x = y
46 45 eximdv ⊢ ∃ x φ → ∃ y ∀ x φ → x = y → ∃ y ∀ x φ ↔ x = y
47 46 com12 ⊢ ∃ y ∀ x φ → x = y → ∃ x φ → ∃ y ∀ x φ ↔ x = y
48 15 47 impbii ⊢ ∃ x φ → ∃ y ∀ x φ ↔ x = y ↔ ∃ y ∀ x φ → x = y
49 48 anbi2i ⊢ ∃ x φ ∧ ∃ x φ → ∃ y ∀ x φ ↔ x = y ↔ ∃ x φ ∧ ∃ y ∀ x φ → x = y
50 abai ⊢ ∃ x φ ∧ ∃ y ∀ x φ ↔ x = y ↔ ∃ x φ ∧ ∃ x φ → ∃ y ∀ x φ ↔ x = y
51 eu3v ⊢ ∃! x φ ↔ ∃ x φ ∧ ∃ y ∀ x φ → x = y
52 49 50 51 3bitr4ri ⊢ ∃! x φ ↔ ∃ x φ ∧ ∃ y ∀ x φ ↔ x = y
53 abai ⊢ ∃ y ∀ x φ ↔ x = y ∧ ∃ x φ ↔ ∃ y ∀ x φ ↔ x = y ∧ ∃ y ∀ x φ ↔ x = y → ∃ x φ
54 ancom ⊢ ∃ x φ ∧ ∃ y ∀ x φ ↔ x = y ↔ ∃ y ∀ x φ ↔ x = y ∧ ∃ x φ
55 biimpr ⊢ φ ↔ x = y → x = y → φ
56 55 alimi ⊢ ∀ x φ ↔ x = y → ∀ x x = y → φ
57 56 eximi ⊢ ∃ y ∀ x φ ↔ x = y → ∃ y ∀ x x = y → φ
58 exsbim ⊢ ∃ y ∀ x x = y → φ → ∃ x φ
59 57 58 syl ⊢ ∃ y ∀ x φ ↔ x = y → ∃ x φ
60 59 biantru ⊢ ∃ y ∀ x φ ↔ x = y ↔ ∃ y ∀ x φ ↔ x = y ∧ ∃ y ∀ x φ ↔ x = y → ∃ x φ
61 53 54 60 3bitr4i ⊢ ∃ x φ ∧ ∃ y ∀ x φ ↔ x = y ↔ ∃ y ∀ x φ ↔ x = y
62 52 61 bitri ⊢ ∃! x φ ↔ ∃ y ∀ x φ ↔ x = y