Theorem brvvdif

Description: Binary relation with the complement under the universal class of ordered pairs. (Contributed by Peter Mazsa, 9-Nov-2018)

	Ref	Expression
Assertion	brvvdif	|- ( ( A e. V /\ B e. W ) -> ( A ( ( _V X. _V ) \ R ) B <-> -. A R B ) )

Proof

Step	Hyp	Ref	Expression
1		opelvvdif	|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. ( ( _V X. _V ) \ R ) <-> -. <. A , B >. e. R ) )
2		df-br	|- ( A ( ( _V X. _V ) \ R ) B <-> <. A , B >. e. ( ( _V X. _V ) \ R ) )
3		df-br	|- ( A R B <-> <. A , B >. e. R )
4	3	notbii	|- ( -. A R B <-> -. <. A , B >. e. R )
5	1 2 4	3bitr4g	|- ( ( A e. V /\ B e. W ) -> ( A ( ( _V X. _V ) \ R ) B <-> -. A R B ) )