This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjresin

Description: The restriction to a disjoint is the empty class. (Contributed by Peter Mazsa, 24-Jul-2024)

		Ref	Expression
	Assertion	disjresin	$⊢ A \cap B = \emptyset \to {R ↾}_{(A \cap B)} = \emptyset$

Step	Hyp	Ref	Expression
1		reseq2	$⊢ A \cap B = \emptyset \to {R ↾}_{(A \cap B)} = {R ↾}_{\emptyset}$
2		res0	$⊢ {R ↾}_{\emptyset} = \emptyset$
3	1 2	eqtrdi	$⊢ A \cap B = \emptyset \to {R ↾}_{(A \cap B)} = \emptyset$