![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brin | Structured version Visualization version GIF version |
Description: The intersection of two relations. (Contributed by FL, 7-Oct-2008.) |
Ref | Expression |
---|---|
brin | ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin 3979 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝑅 ∩ 𝑆) ↔ (〈𝐴, 𝐵〉 ∈ 𝑅 ∧ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
2 | df-br 5149 | . 2 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝑅 ∩ 𝑆)) | |
3 | df-br 5149 | . . 3 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
4 | df-br 5149 | . . 3 ⊢ (𝐴𝑆𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆) | |
5 | 3, 4 | anbi12i 628 | . 2 ⊢ ((𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵) ↔ (〈𝐴, 𝐵〉 ∈ 𝑅 ∧ 〈𝐴, 𝐵〉 ∈ 𝑆)) |
6 | 1, 2, 5 | 3bitr4i 303 | 1 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∧ wa 395 ∈ wcel 2106 ∩ cin 3962 〈cop 4637 class class class wbr 5148 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-in 3970 df-br 5149 |
This theorem is referenced by: brinxp2 5766 trin2 6146 poirr2 6147 dfpo2 6318 predtrss 6345 tpostpos 8270 brinxper 8773 erinxp 8830 sbthcl 9134 infxpenlem 10051 fpwwe2lem11 10679 fpwwe2 10681 isinv 17808 isffth2 17970 ffthf1o 17973 ffthoppc 17978 ffthres2c 17994 isunit 20390 opsrtoslem2 22098 posrasymb 32940 trleile 32946 satefvfmla1 35410 brtxp 35862 idsset 35872 dfon3 35874 elfix 35885 dffix2 35887 brcap 35922 funpartlem 35924 trer 36299 fneval 36335 brcnvin 38352 brxrn 38356 brin2 38391 br1cossinres 38429 grumnud 44282 |
Copyright terms: Public domain | W3C validator |