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

Metamath Proof Explorer

Theorem brelg

Description: Two things in a binary relation belong to the relation's domain. (Contributed by Thierry Arnoux, 29-Aug-2017)

		Ref	Expression
	Assertion	brelg	$⊢ (R \subseteq C \times D \land A R B) \to (A \in C \land B \in D)$

Step	Hyp	Ref	Expression
1		ssbr	$⊢ R \subseteq C \times D \to (A R B \to A (C \times D) B)$
2	1	imp	$⊢ (R \subseteq C \times D \land 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	$⊢ (R \subseteq C \times D \land A R B) \to (A \in C \land B \in D)$