Theorem brin 5201

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 3965	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ∩ 𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 5150	. 2 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ∩ 𝑆))
3		df-br 5150	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4		df-br 5150	. . 3 ⊢ (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
5	3, 4	anbi12i 625	. 2 ⊢ ((𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
6	1, 2, 5	3bitr4i 302	1 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵))

Syntax hints:   ↔ wb 205   ∧ wa 394   ∈ wcel 2104   ∩ cin 3948  ⟨cop 4635   class class class wbr 5149

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3956  df-br 5150

This theorem is referenced by:  brinxp2  5754  trin2  6125  poirr2  6126  dfpo2  6296  predtrss  6324  tpostpos  8235  erinxp  8789  sbthcl  9099  infxpenlem  10012  fpwwe2lem11  10640  fpwwe2  10642  isinv  17713  isffth2  17873  ffthf1o  17876  ffthoppc  17881  ffthres2c  17897  isunit  20266  opsrtoslem2  21838  posrasymb  32400  trleile  32406  satefvfmla1  34712  brtxp  35154  idsset  35164  dfon3  35166  elfix  35177  dffix2  35179  brcap  35214  funpartlem  35216  trer  35506  fneval  35542  brcnvin  37545  brxrn  37549  brin2  37584  br1cossinres  37622  grumnud  43349