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	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\leftrightarrow \exists z\forall x\left(\phi \leftrightarrow x=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		equequ2	$$⊢y=w\to \left(x=y\leftrightarrow x=w\right)$$
2	1	bibi2d	$$⊢y=w\to \left(\left(\phi \leftrightarrow x=y\right)\leftrightarrow \left(\phi \leftrightarrow x=w\right)\right)$$
3	2	albidv	$$⊢y=w\to \left(\forall x\left(\phi \leftrightarrow x=y\right)\leftrightarrow \forall x\left(\phi \leftrightarrow x=w\right)\right)$$
4	3	cbvexvw	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\leftrightarrow \exists w\forall x\left(\phi \leftrightarrow x=w\right)$$
5		equequ2	$$⊢w=z\to \left(x=w\leftrightarrow x=z\right)$$
6	5	bibi2d	$$⊢w=z\to \left(\left(\phi \leftrightarrow x=w\right)\leftrightarrow \left(\phi \leftrightarrow x=z\right)\right)$$
7	6	albidv	$$⊢w=z\to \left(\forall x\left(\phi \leftrightarrow x=w\right)\leftrightarrow \forall x\left(\phi \leftrightarrow x=z\right)\right)$$
8	7	cbvexvw	$$⊢\exists w\forall x\left(\phi \leftrightarrow x=w\right)\leftrightarrow \exists z\forall x\left(\phi \leftrightarrow x=z\right)$$
9	4 8	bitri	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\leftrightarrow \exists z\forall x\left(\phi \leftrightarrow x=z\right)$$