Theorem brdif 4446

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 3400	. 2 |- ( <. A , B >. e. ( R \ S ) <-> ( <. A , B >. e. R /\ -. <. A , B >. e. S ) )
2		df-br 4396	. 2 |- ( A ( R \ S ) B <-> <. A , B >. e. ( R \ S ) )
3		df-br 4396	. . 3 |- ( A R B <-> <. A , B >. e. R )
4		df-br 4396	. . . 4 |- ( A S B <-> <. A , B >. e. S )
5	4	notbii 303	. . 3 |- ( -. A S B <-> -. <. A , B >. e. S )
6	3, 5	anbi12i 711	. 2 |- ( ( A R B /\ -. A S B ) <-> ( <. A , B >. e. R /\ -. <. A , B >. e. S ) )
7	1, 2, 6	3bitr4i 285	1 |- ( A ( R \ S ) B <-> ( A R B /\ -. A S B ) )

Syntax hints:   -. wn 3   <-> wb 189   /\ wa 376   e. wcel 1904   \ cdif 3387   <.cop 3965   class class class wbr 4395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-dif 3393  df-br 4396

This theorem is referenced by:  fndmdif  6001  isocnv3  6241  brdifun  7408  dflt2  11470  pltval  16284  ltgov  24721  opeldifid  28286  qtophaus  28737  dftr6  30461  dffr5  30464  fundmpss  30478  brsset  30727  dfon3  30730  brtxpsd2  30733  dffun10  30752  elfuns  30753  dfrecs2  30788  dfrdg4  30789  dfint3  30790  brub  30792  broutsideof  30959  frege124d  36424