Theorem mojust

Description: Soundness justification theorem for df-mo . (Contributed by NM, 11-Mar-2010) Added this theorem by adapting the proof of eujust . (Revised by BJ, 30-Sep-2022)

	Ref	Expression
Assertion	mojust	$$⊢\exists y\forall x\left(\phi \to x=y\right)\leftrightarrow \exists z\forall x\left(\phi \to x=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		equequ2	$$⊢y=z\to \left(x=y\leftrightarrow x=z\right)$$
2	1	imbi2d	$$⊢y=z\to \left(\left(\phi \to x=y\right)\leftrightarrow \left(\phi \to x=z\right)\right)$$
3	2	albidv	$$⊢y=z\to \left(\forall x\left(\phi \to x=y\right)\leftrightarrow \forall x\left(\phi \to x=z\right)\right)$$
4	3	cbvexvw	$$⊢\exists y\forall x\left(\phi \to x=y\right)\leftrightarrow \exists z\forall x\left(\phi \to x=z\right)$$