Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mojust Structured version   Visualization version   GIF version

Theorem mojust 2615
 Description: Soundness justification theorem for df-mo 2616 (note that 𝑦 and 𝑧 need not be disjoint, although the weaker theorem with that disjoint variable condition added would be enough to justify the soundness of the definition). (Contributed by NM, 11-Mar-2010.) Added this theorem by adapting the proof of eujust 2650. (Revised by BJ, 30-Sep-2022.)
Assertion
Ref Expression
mojust (∃𝑦𝑥(𝜑𝑥 = 𝑦) ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
Distinct variable groups:   𝑥,𝑦   𝑥,𝑧   𝜑,𝑦   𝜑,𝑧
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem mojust
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 equequ2 2026 . . . . 5 (𝑦 = 𝑡 → (𝑥 = 𝑦𝑥 = 𝑡))
21imbi2d 343 . . . 4 (𝑦 = 𝑡 → ((𝜑𝑥 = 𝑦) ↔ (𝜑𝑥 = 𝑡)))
32albidv 1914 . . 3 (𝑦 = 𝑡 → (∀𝑥(𝜑𝑥 = 𝑦) ↔ ∀𝑥(𝜑𝑥 = 𝑡)))
43cbvexvw 2037 . 2 (∃𝑦𝑥(𝜑𝑥 = 𝑦) ↔ ∃𝑡𝑥(𝜑𝑥 = 𝑡))
5 equequ2 2026 . . . . 5 (𝑡 = 𝑧 → (𝑥 = 𝑡𝑥 = 𝑧))
65imbi2d 343 . . . 4 (𝑡 = 𝑧 → ((𝜑𝑥 = 𝑡) ↔ (𝜑𝑥 = 𝑧)))
76albidv 1914 . . 3 (𝑡 = 𝑧 → (∀𝑥(𝜑𝑥 = 𝑡) ↔ ∀𝑥(𝜑𝑥 = 𝑧)))
87cbvexvw 2037 . 2 (∃𝑡𝑥(𝜑𝑥 = 𝑡) ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
94, 8bitri 277 1 (∃𝑦𝑥(𝜑𝑥 = 𝑦) ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1528  ∃wex 1773 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator