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

Theorem brin 4702
Description: The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
Assertion
Ref Expression
brin (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))

Proof of Theorem brin
StepHypRef Expression
1 elin 3794 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 4652 . 2 (𝐴(𝑅𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆))
3 df-br 4652 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4 df-br 4652 . . 3 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
53, 4anbi12i 733 . 2 ((𝐴𝑅𝐵𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
61, 2, 53bitr4i 292 1 (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wcel 1989  cin 3571  cop 4181   class class class wbr 4651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-in 3579  df-br 4652
This theorem is referenced by:  brinxp2  5178  trin2  5517  poirr2  5518  tpostpos  7369  erinxp  7818  sbthcl  8079  infxpenlem  8833  fpwwe2lem12  9460  fpwwe2  9462  isinv  16414  isffth2  16570  ffthf1o  16573  ffthoppc  16578  ffthres2c  16594  isunit  18651  opsrtoslem2  19479  posrasymb  29642  trleile  29651  dfpo2  31631  brtxp  31971  idsset  31981  dfon3  31983  elfix  31994  dffix2  31996  brcap  32031  funpartlem  32033  trer  32294  fneval  32331
  Copyright terms: Public domain W3C validator