Theorem termcbasmo

Description: Two objects in a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypotheses	termcbas.c	No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
	termcbas.b	$$⊢B={\mathrm{Base}}_C$$
	termcbasmo.x	$$⊢\phi \to X\in B$$
	termcbasmo.y	$$⊢\phi \to Y\in B$$
Assertion	termcbasmo	$$⊢\phi \to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		termcbas.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
2		termcbas.b	$$⊢B={\mathrm{Base}}_C$$
3		termcbasmo.x	$$⊢\phi \to X\in B$$
4		termcbasmo.y	$$⊢\phi \to Y\in B$$
5		eqeq1	$$⊢x=X\to \left(x=y\leftrightarrow X=y\right)$$
6		eqeq2	$$⊢y=Y\to \left(X=y\leftrightarrow X=Y\right)$$
7	1 2	termcbas	$$⊢\phi \to \exists zB=\left\{z\right\}$$
8		mosn	$$⊢B=\left\{z\right\}\to {\exists }^{*}xx\in B$$
9	8	exlimiv	$$⊢\exists zB=\left\{z\right\}\to {\exists }^{*}xx\in B$$
10	7 9	syl	$$⊢\phi \to {\exists }^{*}xx\in B$$
11		moel	$$⊢{\exists }^{*}xx\in B\leftrightarrow \forall x\in B\forall y\in Bx=y$$
12	10 11	sylib	$$⊢\phi \to \forall x\in B\forall y\in Bx=y$$
13	5 6 12 3 4	rspc2dv	$$⊢\phi \to X=Y$$