Metamath Proof Explorer

Theorem reldisjunOLD

Description: Obsolete version of reldmun as of 20-Jun-2026. (Contributed by Thierry Arnoux, 9-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	reldisjunOLD	$⊢ (Rel R \land dom R = A \cup B \land A \cap B = \emptyset) \to R = ({R ↾}_{A}) \cup ({R ↾}_{B})$

Proof

Step	Hyp	Ref	Expression
1		reseq2	$⊢ dom R = A \cup B \to {R ↾}_{dom R} = {R ↾}_{(A \cup B)}$
2	1	3ad2ant2	$⊢ (Rel R \land dom R = A \cup B \land A \cap B = \emptyset) \to {R ↾}_{dom R} = {R ↾}_{(A \cup B)}$
3		resdm	$⊢ Rel R \to {R ↾}_{dom R} = R$
4	3	3ad2ant1	$⊢ (Rel R \land dom R = A \cup B \land A \cap B = \emptyset) \to {R ↾}_{dom R} = R$
5		resundi	$⊢ {R ↾}_{(A \cup B)} = ({R ↾}_{A}) \cup ({R ↾}_{B})$
6	5	a1i	$⊢ (Rel R \land dom R = A \cup B \land A \cap B = \emptyset) \to {R ↾}_{(A \cup B)} = ({R ↾}_{A}) \cup ({R ↾}_{B})$
7	2 4 6	3eqtr3d	$⊢ (Rel R \land dom R = A \cup B \land A \cap B = \emptyset) \to R = ({R ↾}_{A}) \cup ({R ↾}_{B})$