Theorem domnrcan

Description: Right-cancellation law for domains. (Contributed by SN, 21-Jun-2025)

	Ref	Expression
Hypotheses	domnrcan.b	$$⊢B={\mathrm{Base}}_R$$
	domnrcan.0	$$⊢\underset{\dot{}}{0}=0_R$$
	domnrcan.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	domnrcan.x	$$⊢\phi \to X\in B$$
	domnrcan.y	$$⊢\phi \to Y\in B$$
	domnrcan.z	$$⊢\phi \to Z\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	domnrcan.r	$$⊢\phi \to R\in \mathrm{Domn}$$
	domnrcan.1	$$⊢\phi \to X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z$$
Assertion	domnrcan	$$⊢\phi \to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		domnrcan.b	$$⊢B={\mathrm{Base}}_R$$
2		domnrcan.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		domnrcan.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		domnrcan.x	$$⊢\phi \to X\in B$$
5		domnrcan.y	$$⊢\phi \to Y\in B$$
6		domnrcan.z	$$⊢\phi \to Z\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
7		domnrcan.r	$$⊢\phi \to R\in \mathrm{Domn}$$
8		domnrcan.1	$$⊢\phi \to X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z$$
9	1 2 3 4 5 6 7	domnrcanb	$$⊢\phi \to \left(X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z\leftrightarrow X=Y\right)$$
10	8 9	mpbid	$$⊢\phi \to X=Y$$