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\mathrm{V}B$$

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
2		df-br	$$⊢A\mathrm{V}B\leftrightarrow ⟨A,B⟩\in \mathrm{V}$$
3	1 2	mpbir	$$⊢A\mathrm{V}B$$