Metamath Proof Explorer

Theorem eujust

Description: Soundness justification theorem for eu6 when this was the definition of the unique existential quantifier (note that y and z need not be disjoint, although the weaker theorem with that disjoint variable condition added would be enough to justify the soundness of the definition). See eujustALT for a proof that provides an example of how it can be achieved through the use of dvelim . (Contributed by NM, 11-Mar-2010) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion eujust ⊢∃y∀xφ↔x=y↔∃z∀xφ↔x=z

Proof

Step Hyp Ref Expression
1 equequ2 ⊢y=w→x=y↔x=w
2 1 bibi2d ⊢y=w→φ↔x=y↔φ↔x=w
3 2 albidv ⊢y=w→∀xφ↔x=y↔∀xφ↔x=w
4 3 cbvexvw ⊢∃y∀xφ↔x=y↔∃w∀xφ↔x=w
5 equequ2 ⊢w=z→x=w↔x=z
6 5 bibi2d ⊢w=z→φ↔x=w↔φ↔x=z
7 6 albidv ⊢w=z→∀xφ↔x=w↔∀xφ↔x=z
8 7 cbvexvw ⊢∃w∀xφ↔x=w↔∃z∀xφ↔x=z
9 4 8 bitri ⊢∃y∀xφ↔x=y↔∃z∀xφ↔x=z