Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  brdif Structured version   Visualization version   GIF version

Theorem brdif 4982
 Description: The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
Assertion
Ref Expression
brdif (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))

Proof of Theorem brdif
StepHypRef Expression
1 eldif 3839 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 4930 . 2 (𝐴(𝑅𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆))
3 df-br 4930 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4 df-br 4930 . . . 4 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
54notbii 312 . . 3 𝐴𝑆𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
63, 5anbi12i 617 . 2 ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
71, 2, 63bitr4i 295 1 (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 387   ∈ wcel 2050   ∖ cdif 3826  ⟨cop 4447   class class class wbr 4929 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-dif 3832  df-br 4930 This theorem is referenced by:  fundif  6236  fndmdif  6637  isocnv3  6908  brdifun  8118  dflt2  12358  pltval  17428  ltgov  26085  opeldifid  30115  qtophaus  30750  dftr6  32512  dffr5  32515  fundmpss  32535  slenlt  32758  brsset  32877  dfon3  32880  brtxpsd2  32883  dffun10  32902  elfuns  32903  dfrecs2  32938  dfrdg4  32939  dfint3  32940  brub  32942  broutsideof  33109  brvdif  34972  frege124d  39475
 Copyright terms: Public domain W3C validator