![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > breq | Structured version Visualization version GIF version |
Description: Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.) |
Ref | Expression |
---|---|
breq | ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2871 | . 2 ⊢ (𝑅 = 𝑆 → (〈𝐴, 𝐵〉 ∈ 𝑅 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
2 | df-br 4963 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
3 | df-br 4963 | . 2 ⊢ (𝐴𝑆𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆) | |
4 | 1, 2, 3 | 3bitr4g 315 | 1 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1522 ∈ wcel 2081 〈cop 4478 class class class wbr 4962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 df-cleq 2788 df-clel 2863 df-br 4963 |
This theorem is referenced by: breqi 4968 breqd 4973 poeq1 5365 soeq1 5382 freq1 5413 fveq1 6537 foeqcnvco 6921 f1eqcocnv 6922 isoeq2 6934 isoeq3 6935 brfvopab 7070 ofreq 7270 supeq3 8759 oieq1 8822 dcomex 9715 axdc2lem 9716 brdom3 9796 brdom7disj 9799 brdom6disj 9800 dfrtrclrec2 14250 relexpindlem 14256 rtrclind 14258 shftfval 14263 isprs 17369 isdrs 17373 ispos 17386 istos 17474 efglem 18569 frgpuplem 18625 ordtval 21481 utop2nei 22542 utop3cls 22543 isucn2 22571 ucnima 22573 iducn 22575 ex-opab 27903 resspos 30320 acycgr0v 32004 prclisacycgr 32007 satf 32209 eqfunresadj 32613 cureq 34418 poimirlem31 34473 poimir 34475 cosseq 35221 elrefrels3 35308 elcnvrefrels3 35321 elsymrels3 35340 elsymrels5 35342 eltrrels3 35366 eleqvrels3 35378 brabsb2 35548 rfovfvd 39852 fsovrfovd 39859 sprsymrelf 43159 sprsymrelfo 43161 upwlkbprop 43515 |
Copyright terms: Public domain | W3C validator |