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	⊢ 𝐴 V 𝐵

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
2		df-br	⊢ ( 𝐴 V 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ V )
3	1 2	mpbir	⊢ 𝐴 V 𝐵