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

Theorem brdif 5196
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 3961 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 5144 . 2 (𝐴(𝑅𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆))
3 df-br 5144 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4 df-br 5144 . . . 4 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
54notbii 320 . . 3 𝐴𝑆𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
63, 5anbi12i 628 . 2 ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
71, 2, 63bitr4i 303 1 (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395  wcel 2108  cdif 3948  cop 4632   class class class wbr 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-br 5144
This theorem is referenced by:  fundif  6615  fndmdif  7062  isocnv3  7352  brdifun  8775  dflt2  13190  pltval  18377  slenlt  27797  ltgov  28605  opeldifid  32612  qtophaus  33835  dftr6  35751  dffr5  35754  fundmpss  35767  brsset  35890  dfon3  35893  brtxpsd2  35896  dffun10  35915  elfuns  35916  dfrecs2  35951  dfrdg4  35952  dfint3  35953  brub  35955  broutsideof  36122  brvdif  38262  frege124d  43774
  Copyright terms: Public domain W3C validator