Metamath Proof Explorer


Theorem brdif

Description: The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011)

Ref Expression
Assertion brdif
|- ( A ( R \ S ) B <-> ( A R B /\ -. A S B ) )

Proof

Step Hyp Ref Expression
1 eldif
 |-  ( <. A , B >. e. ( R \ S ) <-> ( <. A , B >. e. R /\ -. <. A , B >. e. S ) )
2 df-br
 |-  ( A ( R \ S ) B <-> <. A , B >. e. ( R \ S ) )
3 df-br
 |-  ( A R B <-> <. A , B >. e. R )
4 df-br
 |-  ( A S B <-> <. A , B >. e. S )
5 4 notbii
 |-  ( -. A S B <-> -. <. A , B >. e. S )
6 3 5 anbi12i
 |-  ( ( A R B /\ -. A S B ) <-> ( <. A , B >. e. R /\ -. <. A , B >. e. S ) )
7 1 2 6 3bitr4i
 |-  ( A ( R \ S ) B <-> ( A R B /\ -. A S B ) )