Metamath Proof Explorer

Theorem regsfromregtr

Description: Derivation of ax-regs from ax-reg + exeltr . (Contributed by Matthew House, 4-Mar-2026)

Ref Expression
Hypotheses regsfromregtr.1 ⊢ ( ∃ 𝑦 𝑦 ∈ 𝑤 → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) )
regsfromregtr.2 ⊢ ∃ 𝑢 ( 𝑣 ∈ 𝑢 ∧ ∀ 𝑡 ( 𝑡 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢 ) ) )
Assertion regsfromregtr ( ∃ 𝑥 𝜑 → ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )

Proof

Step Hyp Ref Expression
1 regsfromregtr.1 ⊢ ( ∃ 𝑦 𝑦 ∈ 𝑤 → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) )
2 regsfromregtr.2 ⊢ ∃ 𝑢 ( 𝑣 ∈ 𝑢 ∧ ∀ 𝑡 ( 𝑡 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢 ) ) )
3 vex ⊢ 𝑣 ∈ V
4 elequ1 ⊢ ( 𝑦 = 𝑣 → ( 𝑦 ∈ 𝑢 ↔ 𝑣 ∈ 𝑢 ) )
5 sbequ ⊢ ( 𝑦 = 𝑣 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑣 / 𝑥 ] 𝜑 ) )
6 4 5 anbi12d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝑣 ∈ 𝑢 ∧ [ 𝑣 / 𝑥 ] 𝜑 ) ) )
7 3 6 spcev ⊢ ( ( 𝑣 ∈ 𝑢 ∧ [ 𝑣 / 𝑥 ] 𝜑 ) → ∃ 𝑦 ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
8 7 adantlr ⊢ ( ( ( 𝑣 ∈ 𝑢 ∧ Tr 𝑢 ) ∧ [ 𝑣 / 𝑥 ] 𝜑 ) → ∃ 𝑦 ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
9 vex ⊢ 𝑢 ∈ V
10 9 rabex ⊢ { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } ∈ V
11 eleq2 ⊢ ( 𝑤 = { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } ) )
12 sbequ ⊢ ( 𝑟 = 𝑦 → ( [ 𝑟 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
13 12 elrab ⊢ ( 𝑦 ∈ { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } ↔ ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
14 11 13 bitrdi ⊢ ( 𝑤 = { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } → ( 𝑦 ∈ 𝑤 ↔ ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
15 14 exbidv ⊢ ( 𝑤 = { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } → ( ∃ 𝑦 𝑦 ∈ 𝑤 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
16 eleq2 ⊢ ( 𝑤 = { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } ) )
17 sbequ ⊢ ( 𝑟 = 𝑧 → ( [ 𝑟 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
18 17 elrab ⊢ ( 𝑧 ∈ { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } ↔ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
19 16 18 bitrdi ⊢ ( 𝑤 = { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } → ( 𝑧 ∈ 𝑤 ↔ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
20 19 notbid ⊢ ( 𝑤 = { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } → ( ¬ 𝑧 ∈ 𝑤 ↔ ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
21 20 imbi2d ⊢ ( 𝑤 = { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } → ( ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ↔ ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) )
22 21 albidv ⊢ ( 𝑤 = { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) )
23 14 22 anbi12d ⊢ ( 𝑤 = { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } → ( ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) ↔ ( ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) ) )
24 23 exbidv ⊢ ( 𝑤 = { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } → ( ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) ↔ ∃ 𝑦 ( ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) ) )
25 15 24 imbi12d ⊢ ( 𝑤 = { 𝑟 ∈ 𝑢 ∣ [ 𝑟 / 𝑥 ] 𝜑 } → ( ( ∃ 𝑦 𝑦 ∈ 𝑤 → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) ) ↔ ( ∃ 𝑦 ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ∃ 𝑦 ( ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) ) ) )
26 10 25 1 vtocl ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ∃ 𝑦 ( ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) )
27 8 26 syl ⊢ ( ( ( 𝑣 ∈ 𝑢 ∧ Tr 𝑢 ) ∧ [ 𝑣 / 𝑥 ] 𝜑 ) → ∃ 𝑦 ( ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) )
28 imnan ⊢ ( ( 𝑧 ∈ 𝑢 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
29 trel ⊢ ( Tr 𝑢 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑢 ) → 𝑧 ∈ 𝑢 ) )
30 29 imp ⊢ ( ( Tr 𝑢 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑢 ) ) → 𝑧 ∈ 𝑢 )
31 30 anass1rs ⊢ ( ( ( Tr 𝑢 ∧ 𝑦 ∈ 𝑢 ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝑢 )
32 imbibi ⊢ ( ( ( 𝑧 ∈ 𝑢 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) → ( 𝑧 ∈ 𝑢 → ( ¬ [ 𝑧 / 𝑥 ] 𝜑 ↔ ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) )
33 28 31 32 mpsyl ⊢ ( ( ( Tr 𝑢 ∧ 𝑦 ∈ 𝑢 ) ∧ 𝑧 ∈ 𝑦 ) → ( ¬ [ 𝑧 / 𝑥 ] 𝜑 ↔ ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
34 33 pm5.74da ⊢ ( ( Tr 𝑢 ∧ 𝑦 ∈ 𝑢 ) → ( ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) )
35 34 albidv ⊢ ( ( Tr 𝑢 ∧ 𝑦 ∈ 𝑢 ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) )
36 35 biimpar ⊢ ( ( ( Tr 𝑢 ∧ 𝑦 ∈ 𝑢 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) → ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) )
37 36 anim2i ⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ( ( Tr 𝑢 ∧ 𝑦 ∈ 𝑢 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) ) → ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
38 37 exp44 ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ( Tr 𝑢 → ( 𝑦 ∈ 𝑢 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) → ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) ) ) )
39 38 com3l ⊢ ( Tr 𝑢 → ( 𝑦 ∈ 𝑢 → ( [ 𝑦 / 𝑥 ] 𝜑 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) → ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) ) ) )
40 39 imp4c ⊢ ( Tr 𝑢 → ( ( ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) → ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) )
41 40 eximdv ⊢ ( Tr 𝑢 → ( ∃ 𝑦 ( ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) → ∃ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) )
42 41 ad2antlr ⊢ ( ( ( 𝑣 ∈ 𝑢 ∧ Tr 𝑢 ) ∧ [ 𝑣 / 𝑥 ] 𝜑 ) → ( ∃ 𝑦 ( ( 𝑦 ∈ 𝑢 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ( 𝑧 ∈ 𝑢 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) → ∃ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) )
43 27 42 mpd ⊢ ( ( ( 𝑣 ∈ 𝑢 ∧ Tr 𝑢 ) ∧ [ 𝑣 / 𝑥 ] 𝜑 ) → ∃ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
44 43 ex ⊢ ( ( 𝑣 ∈ 𝑢 ∧ Tr 𝑢 ) → ( [ 𝑣 / 𝑥 ] 𝜑 → ∃ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) )
45 dftr3 ⊢ ( Tr 𝑢 ↔ ∀ 𝑡 ∈ 𝑢 𝑡 ⊆ 𝑢 )
46 df-ss ⊢ ( 𝑡 ⊆ 𝑢 ↔ ∀ 𝑠 ( 𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢 ) )
47 46 ralbii ⊢ ( ∀ 𝑡 ∈ 𝑢 𝑡 ⊆ 𝑢 ↔ ∀ 𝑡 ∈ 𝑢 ∀ 𝑠 ( 𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢 ) )
48 df-ral ⊢ ( ∀ 𝑡 ∈ 𝑢 ∀ 𝑠 ( 𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢 ) ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢 ) ) )
49 45 47 48 3bitri ⊢ ( Tr 𝑢 ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢 ) ) )
50 49 anbi2i ⊢ ( ( 𝑣 ∈ 𝑢 ∧ Tr 𝑢 ) ↔ ( 𝑣 ∈ 𝑢 ∧ ∀ 𝑡 ( 𝑡 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢 ) ) ) )
51 50 exbii ⊢ ( ∃ 𝑢 ( 𝑣 ∈ 𝑢 ∧ Tr 𝑢 ) ↔ ∃ 𝑢 ( 𝑣 ∈ 𝑢 ∧ ∀ 𝑡 ( 𝑡 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢 ) ) ) )
52 2 51 mpbir ⊢ ∃ 𝑢 ( 𝑣 ∈ 𝑢 ∧ Tr 𝑢 )
53 44 52 exlimiiv ⊢ ( [ 𝑣 / 𝑥 ] 𝜑 → ∃ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
54 53 exlimiv ⊢ ( ∃ 𝑣 [ 𝑣 / 𝑥 ] 𝜑 → ∃ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
55 nfv ⊢ Ⅎ 𝑣 𝜑
56 55 sb8ef ⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑣 [ 𝑣 / 𝑥 ] 𝜑 )
57 56 bicomi ⊢ ( ∃ 𝑣 [ 𝑣 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 𝜑 )
58 sb6 ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
59 sb6 ⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
60 59 notbii ⊢ ( ¬ [ 𝑧 / 𝑥 ] 𝜑 ↔ ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
61 60 imbi2i ⊢ ( ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
62 61 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
63 58 62 anbi12i ⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
64 63 exbii ⊢ ( ∃ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ [ 𝑧 / 𝑥 ] 𝜑 ) ) ↔ ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
65 54 57 64 3imtr3i ⊢ ( ∃ 𝑥 𝜑 → ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )