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

Metamath Proof Explorer

Theorem brrelex1i

Description: The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998)

		Ref	Expression
	Hypothesis	brrelexi.1	$⊢ Rel R$
	Assertion	brrelex1i	$⊢ A R B \to A \in V$

Step	Hyp	Ref	Expression
1		brrelexi.1	$⊢ Rel R$
2		brrelex1	$⊢ (Rel R \land A R B) \to A \in V$
3	1 2	mpan	$⊢ A R B \to A \in V$