Theorem brdif 4363

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

Assertion

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

Proof of Theorem brdif

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

Syntax hints:   -. wn 3   <-> wb 184   /\ wa 369   e. wcel 1756   \ cdif 3346   <.cop 3904   class class class wbr 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-dif 3352  df-br 4314

This theorem is referenced by:  fndmdif  5828  isocnv3  6044  brdifun  7149  dfsup2OLD  7714  dflt2  11146  pltval  15151  dftr6  27582  dffr5  27585  fundmpss  27599  brsset  27942  dfon3  27945  brtxpsd2  27948  dffun10  27967  elfuns  27968  dfrdg4  28003  dfint3  28005  brub  28007  broutsideof  28174