Theorem mndtcob

Description: Lemma for mndtchom and mndtcco . (Contributed by Zhi Wang, 22-Sep-2024) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mndtcbas.c	No typesetting found for |- ( ph -> C = ( MndToCat ` M ) ) with typecode |-
	mndtcbas.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
	mndtcbas.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
	mndtchom.x	$$⊢\phi \to X\in B$$
Assertion	mndtcob	$$⊢\phi \to X=M$$

Proof

Step	Hyp	Ref	Expression
1		mndtcbas.c	Could not format ( ph -> C = ( MndToCat ` M ) ) : No typesetting found for |- ( ph -> C = ( MndToCat ` M ) ) with typecode |-
2		mndtcbas.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
3		mndtcbas.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
4		mndtchom.x	$$⊢\phi \to X\in B$$
5	1 2 3	mndtcbasval	$$⊢\phi \to B=\left\{M\right\}$$
6	4 5	eleqtrd	$$⊢\phi \to X\in \left\{M\right\}$$
7		elsng	$$⊢X\in B\to \left(X\in \left\{M\right\}\leftrightarrow X=M\right)$$
8	4 7	syl	$$⊢\phi \to \left(X\in \left\{M\right\}\leftrightarrow X=M\right)$$
9	6 8	mpbid	$$⊢\phi \to X=M$$