Theorem brvbrvvdif

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

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

Proof

Step	Hyp	Ref	Expression
1		brvvdif	|- ( ( A e. V /\ B e. W ) -> ( A ( ( _V X. _V ) \ R ) B <-> -. A R B ) )
2		brvdif	|- ( A ( _V \ R ) B <-> -. A R B )
3	1 2	bitr4di	|- ( ( A e. V /\ B e. W ) -> ( A ( ( _V X. _V ) \ R ) B <-> A ( _V \ R ) B ) )