Theorem brv

Description: Two classes are always in relation by _V . This is simply equivalent to <. A , B >. e.V , and does not imply that V is a relation: see nrelv . (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Assertion	brv	|- A _V B

Proof

Step	Hyp	Ref	Expression
1		opex	|- <. A , B >. e. _V
2		df-br	|- ( A _V B <-> <. A , B >. e. _V )
3	1 2	mpbir	|- A _V B