| 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 3911 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝑅 ∖ 𝑆) ↔ (〈𝐴, 𝐵〉 ∈ 𝑅 ∧ ¬ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
| 2 | df-br 5099 | . 2 ⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝑅 ∖ 𝑆)) | |
| 3 | df-br 5099 | . . 3 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
| 4 | df-br 5099 | . . . 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 2113 ∖ cdif 3898 〈cop 4586 class class class wbr 5098 |
| 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 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1544 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-v 3442 df-dif 3904 df-br 5099 |
| This theorem is referenced by: fundif 6541 fndmdif 6987 isocnv3 7278 brdifun 8665 dflt2 13062 pltval 18253 lenlts 27720 ltgov 28669 opeldifid 32674 qtophaus 33993 dftr6 35945 dffr5 35948 fundmpss 35961 brsset 36081 dfon3 36084 brtxpsd2 36087 dffun10 36106 elfuns 36107 dfrecs2 36144 dfrdg4 36145 dfint3 36146 brub 36148 broutsideof 36315 brvdif 38459 frege124d 44002 |
| Copyright terms: Public domain | W3C validator |