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

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

Proof of Theorem brin
StepHypRef Expression
1 elin 4173 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 5064 . 2 (𝐴(𝑅𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆))
3 df-br 5064 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4 df-br 5064 . . 3 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
53, 4anbi12i 626 . 2 ((𝐴𝑅𝐵𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
61, 2, 53bitr4i 304 1 (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2107   ∩ cin 3939  ⟨cop 4570   class class class wbr 5063 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-in 3947  df-br 5064 This theorem is referenced by:  brinxp2  5628  trin2  5981  poirr2  5982  tpostpos  7903  erinxp  8361  sbthcl  8628  infxpenlem  9428  fpwwe2lem12  10052  fpwwe2  10054  isinv  17020  isffth2  17176  ffthf1o  17179  ffthoppc  17184  ffthres2c  17200  isunit  19327  opsrtoslem2  20183  posrasymb  30558  trleile  30567  satefvfmla1  32556  dfpo2  32875  brtxp  33225  idsset  33235  dfon3  33237  elfix  33248  dffix2  33250  brcap  33285  funpartlem  33287  trer  33548  fneval  33584  brxrn  35493  brin2  35524  br1cossinres  35554  grumnud  40487
 Copyright terms: Public domain W3C validator