Metamath Proof Explorer

Theorem brrelex1

Description: If two classes are related by a binary relation, then the first class is a set. (Contributed by NM, 18-May-2004) (Revised by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	brrelex1	$⊢ (Rel R \land A R B) \to A \in V$

Proof

Step	Hyp	Ref	Expression
1		brrelex12	$⊢ (Rel R \land A R B) \to (A \in V \land B \in V)$
2	1	simpld	$⊢ (Rel R \land A R B) \to A \in V$