Metamath Proof Explorer


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 V
2 df-br A V B A B V
3 1 2 mpbir A V B