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 ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
eu6w.y ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜃 ) )
Assertion eu6w ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )

Proof

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