![]() |
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 2828 | . 2 ⊢ (𝑅 = 𝑆 → (〈𝐴, 𝐵〉 ∈ 𝑅 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
2 | df-br 5149 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
3 | df-br 5149 | . 2 ⊢ (𝐴𝑆𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆) | |
4 | 1, 2, 3 | 3bitr4g 314 | 1 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 = wceq 1537 ∈ wcel 2106 〈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-ex 1777 df-cleq 2727 df-clel 2814 df-br 5149 |
This theorem is referenced by: breqi 5154 breqd 5159 poeq1 5600 soeq1 5618 freq1 5656 fveq1 6906 foeqcnvco 7320 f1eqcocnv 7321 isoeq2 7338 isoeq3 7339 eqfunresadj 7380 brfvopab 7490 ofreq 7701 supeq3 9487 oieq1 9550 ttrcleq 9747 dcomex 10485 axdc2lem 10486 brdom3 10566 brdom7disj 10569 brdom6disj 10570 dfrtrclrec2 15094 relexpindlem 15099 rtrclind 15101 shftfval 15106 isprs 18354 isdrs 18359 ispos 18372 istos 18476 efglem 19749 frgpuplem 19805 ordtval 23213 utop2nei 24275 utop3cls 24276 isucn2 24304 ucnima 24306 iducn 24308 ex-opab 30461 resspos 32941 acycgr0v 35133 prclisacycgr 35136 satf 35338 cureq 37583 poimirlem31 37638 poimir 37640 cosseq 38408 elrefrels3 38501 elcnvrefrels3 38517 elsymrels3 38536 elsymrels5 38538 eltrrels3 38562 eleqvrels3 38575 brabsb2 38844 rfovfvd 43992 fsovrfovd 43999 sprsymrelf 47420 sprsymrelfo 47422 upwlkbprop 47982 |
Copyright terms: Public domain | W3C validator |