Theorem mojust

Description: Soundness justification theorem for df-mo (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). (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=t\to \left(x=y\leftrightarrow x=t\right)$$
2	1	imbi2d	$$⊢y=t\to \left(\left(\phi \to x=y\right)\leftrightarrow \left(\phi \to x=t\right)\right)$$
3	2	albidv	$$⊢y=t\to \left(\forall x\left(\phi \to x=y\right)\leftrightarrow \forall x\left(\phi \to x=t\right)\right)$$
4	3	cbvexvw	$$⊢\exists y\forall x\left(\phi \to x=y\right)\leftrightarrow \exists t\forall x\left(\phi \to x=t\right)$$
5		equequ2	$$⊢t=z\to \left(x=t\leftrightarrow x=z\right)$$
6	5	imbi2d	$$⊢t=z\to \left(\left(\phi \to x=t\right)\leftrightarrow \left(\phi \to x=z\right)\right)$$
7	6	albidv	$$⊢t=z\to \left(\forall x\left(\phi \to x=t\right)\leftrightarrow \forall x\left(\phi \to x=z\right)\right)$$
8	7	cbvexvw	$$⊢\exists t\forall x\left(\phi \to x=t\right)\leftrightarrow \exists z\forall x\left(\phi \to x=z\right)$$
9	4 8	bitri	$$⊢\exists y\forall x\left(\phi \to x=y\right)\leftrightarrow \exists z\forall x\left(\phi \to x=z\right)$$