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 2898 | . 2 ⊢ (𝑅 = 𝑆 → (〈𝐴, 𝐵〉 ∈ 𝑅 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
2 | df-br 5058 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
3 | df-br 5058 | . 2 ⊢ (𝐴𝑆𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆) | |
4 | 1, 2, 3 | 3bitr4g 315 | 1 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 〈cop 4563 class class class wbr 5057 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 df-br 5058 |
This theorem is referenced by: breqi 5063 breqd 5068 poeq1 5470 soeq1 5487 freq1 5518 fveq1 6662 foeqcnvco 7047 f1eqcocnv 7048 isoeq2 7060 isoeq3 7061 brfvopab 7200 ofreq 7401 supeq3 8901 oieq1 8964 dcomex 9857 axdc2lem 9858 brdom3 9938 brdom7disj 9941 brdom6disj 9942 dfrtrclrec2 14404 relexpindlem 14410 rtrclind 14412 shftfval 14417 isprs 17528 isdrs 17532 ispos 17545 istos 17633 efglem 18771 frgpuplem 18827 ordtval 21725 utop2nei 22786 utop3cls 22787 isucn2 22815 ucnima 22817 iducn 22819 ex-opab 28138 resspos 30573 acycgr0v 32292 prclisacycgr 32295 satf 32497 eqfunresadj 32901 cureq 34749 poimirlem31 34804 poimir 34806 cosseq 35551 elrefrels3 35638 elcnvrefrels3 35651 elsymrels3 35670 elsymrels5 35672 eltrrels3 35696 eleqvrels3 35708 brabsb2 35878 rfovfvd 40226 fsovrfovd 40233 sprsymrelf 43534 sprsymrelfo 43536 upwlkbprop 43890 |
Copyright terms: Public domain | W3C validator |