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

Metamath Proof Explorer

Theorem brel

Description: Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996) (Revised by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Hypothesis	brel.1	$⊢ R \subseteq C \times D$
	Assertion	brel	$⊢ A R B \to (A \in C \land B \in D)$

Proof

Step	Hyp	Ref	Expression
1		brel.1	$⊢ R \subseteq C \times D$
2	1	ssbri	$⊢ A R B \to A (C \times D) B$
3		brxp	$⊢ A (C \times D) B \leftrightarrow (A \in C \land B \in D)$
4	2 3	sylib	$⊢ A R B \to (A \in C \land B \in D)$