Theorem brdif 5127

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

Assertion

Ref	Expression
brdif	⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))

Proof of Theorem brdif

Step	Hyp	Ref	Expression
1		eldif 3897	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ∖ 𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 5075	. 2 ⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ∖ 𝑆))
3		df-br 5075	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4		df-br 5075	. . . 4 ⊢ (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
5	4	notbii 320	. . 3 ⊢ (¬ 𝐴𝑆𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
6	3, 5	anbi12i 627	. 2 ⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
7	1, 2, 6	3bitr4i 303	1 ⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   ∈ wcel 2106   ∖ cdif 3884  ⟨cop 4567   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-br 5075

This theorem is referenced by:  fundif  6483  fndmdif  6919  isocnv3  7203  brdifun  8527  dflt2  12882  pltval  18050  ltgov  26958  opeldifid  30938  qtophaus  31786  dftr6  33718  dffr5  33721  fundmpss  33740  slenlt  33955  brsset  34191  dfon3  34194  brtxpsd2  34197  dffun10  34216  elfuns  34217  dfrecs2  34252  dfrdg4  34253  dfint3  34254  brub  34256  broutsideof  34423  brvdif  36400  frege124d  41369