Theorem brin 5138

Description: The intersection of two relations. (Contributed by FL, 7-Oct-2008.)

Assertion

Ref	Expression
brin	⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵))

Proof of Theorem brin

Step	Hyp	Ref	Expression
1		elin 3906	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ∩ 𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 5087	. 2 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ∩ 𝑆))
3		df-br 5087	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4		df-br 5087	. . 3 ⊢ (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
5	3, 4	anbi12i 629	. 2 ⊢ ((𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
6	1, 2, 5	3bitr4i 303	1 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   ∩ cin 3889  ⟨cop 4574   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-br 5087

This theorem is referenced by:  brinxp2  5703  trin2  6081  poirr2  6082  dfpo2  6255  predtrss  6281  tpostpos  8190  brinxper  8667  erinxp  8732  sbthcl  9031  infxpenlem  9929  fpwwe2lem11  10558  fpwwe2  10560  isinv  17721  isffth2  17879  ffthf1o  17882  ffthoppc  17887  ffthres2c  17903  isunit  20347  opsrtoslem2  22047  zsoring  28418  posrasymb  33045  trleile  33049  satefvfmla1  35626  brtxp  36079  idsset  36089  dfon3  36091  elfix  36102  dffix2  36104  brcap  36139  funpartlem  36143  trer  36517  fneval  36553  brcnvin  38716  brxrn  38721  brin2  38776  br1cossinres  38875  grumnud  44734