| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > brdif | Structured version Visualization version GIF version | ||
| Description: The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.) |
| Ref | Expression |
|---|---|
| brdif | ⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldif 3910 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝑅 ∖ 𝑆) ↔ (〈𝐴, 𝐵〉 ∈ 𝑅 ∧ ¬ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
| 2 | df-br 5090 | . 2 ⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝑅 ∖ 𝑆)) | |
| 3 | df-br 5090 | . . 3 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
| 4 | df-br 5090 | . . . 4 ⊢ (𝐴𝑆𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆) | |
| 5 | 4 | notbii 320 | . . 3 ⊢ (¬ 𝐴𝑆𝐵 ↔ ¬ 〈𝐴, 𝐵〉 ∈ 𝑆) |
| 6 | 3, 5 | anbi12i 628 | . 2 ⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵) ↔ (〈𝐴, 𝐵〉 ∈ 𝑅 ∧ ¬ 〈𝐴, 𝐵〉 ∈ 𝑆)) |
| 7 | 1, 2, 6 | 3bitr4i 303 | 1 ⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 ∈ wcel 2110 ∖ cdif 3897 〈cop 4580 class class class wbr 5089 |
| 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 2112 ax-9 2120 ax-ext 2702 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1544 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2722 df-clel 2804 df-v 3436 df-dif 3903 df-br 5090 |
| This theorem is referenced by: fundif 6526 fndmdif 6970 isocnv3 7261 brdifun 8647 dflt2 13039 pltval 18228 slenlt 27684 ltgov 28568 opeldifid 32569 qtophaus 33839 dftr6 35763 dffr5 35766 fundmpss 35779 brsset 35902 dfon3 35905 brtxpsd2 35908 dffun10 35927 elfuns 35928 dfrecs2 35963 dfrdg4 35964 dfint3 35965 brub 35967 broutsideof 36134 brvdif 38275 frege124d 43773 |
| Copyright terms: Public domain | W3C validator |