Theorem brdif 4452

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 3413	. 2 |- ( <. A , B >. e. ( R \ S ) <-> ( <. A , B >. e. R /\ -. <. A , B >. e. S ) )
2		df-br 4402	. 2 |- ( A ( R \ S ) B <-> <. A , B >. e. ( R \ S ) )
3		df-br 4402	. . 3 |- ( A R B <-> <. A , B >. e. R )
4		df-br 4402	. . . 4 |- ( A S B <-> <. A , B >. e. S )
5	4	notbii 298	. . 3 |- ( -. A S B <-> -. <. A , B >. e. S )
6	3, 5	anbi12i 702	. 2 |- ( ( A R B /\ -. A S B ) <-> ( <. A , B >. e. R /\ -. <. A , B >. e. S ) )
7	1, 2, 6	3bitr4i 281	1 |- ( A ( R \ S ) B <-> ( A R B /\ -. A S B ) )

Syntax hints:   -. wn 3   <-> wb 188   /\ wa 371   e. wcel 1886   \ cdif 3400   <.cop 3973   class class class wbr 4401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046  df-dif 3406  df-br 4402

This theorem is referenced by:  fndmdif  5984  isocnv3  6221  brdifun  7387  dflt2  11444  pltval  16199  ltgov  24635  opeldifid  28203  qtophaus  28656  dftr6  30383  dffr5  30386  fundmpss  30400  brsset  30649  dfon3  30652  brtxpsd2  30655  dffun10  30674  elfuns  30675  dfrecs2  30710  dfrdg4  30711  dfint3  30712  brub  30714  broutsideof  30881  frege124d  36347