Theorem brin 5148

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113   ∩ cin 3898  ⟨cop 4584   class class class wbr 5096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-br 5097

This theorem is referenced by:  brinxp2  5700  trin2  6078  poirr2  6079  dfpo2  6252  predtrss  6278  tpostpos  8186  brinxper  8662  erinxp  8726  sbthcl  9025  infxpenlem  9921  fpwwe2lem11  10550  fpwwe2  10552  isinv  17682  isffth2  17840  ffthf1o  17843  ffthoppc  17848  ffthres2c  17864  isunit  20307  opsrtoslem2  22009  zsoring  28367  posrasymb  32998  trleile  33002  satefvfmla1  35568  brtxp  36021  idsset  36031  dfon3  36033  elfix  36044  dffix2  36046  brcap  36081  funpartlem  36085  trer  36459  fneval  36495  brcnvin  38502  brxrn  38507  brin2  38562  br1cossinres  38649  grumnud  44469