| 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 2830 | . 2 ⊢ (𝑅 = 𝑆 → (〈𝐴, 𝐵〉 ∈ 𝑅 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
| 2 | df-br 5144 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
| 3 | df-br 5144 | . 2 ⊢ (𝐴𝑆𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆) | |
| 4 | 1, 2, 3 | 3bitr4g 314 | 1 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 〈cop 4632 class class class wbr 5143 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-clel 2816 df-br 5144 |
| This theorem is referenced by: breqi 5149 breqd 5154 poeq1 5595 soeq1 5613 freq1 5652 fveq1 6905 foeqcnvco 7320 f1eqcocnv 7321 isoeq2 7338 isoeq3 7339 eqfunresadj 7380 brfvopab 7490 ofreq 7701 supeq3 9489 oieq1 9552 ttrcleq 9749 dcomex 10487 axdc2lem 10488 brdom3 10568 brdom7disj 10571 brdom6disj 10572 dfrtrclrec2 15097 relexpindlem 15102 rtrclind 15104 shftfval 15109 isprs 18342 isdrs 18347 ispos 18360 istos 18463 efglem 19734 frgpuplem 19790 ordtval 23197 utop2nei 24259 utop3cls 24260 isucn2 24288 ucnima 24290 iducn 24292 ex-opab 30451 resspos 32956 acycgr0v 35153 prclisacycgr 35156 satf 35358 cureq 37603 poimirlem31 37658 poimir 37660 cosseq 38427 elrefrels3 38520 elcnvrefrels3 38536 elsymrels3 38555 elsymrels5 38557 eltrrels3 38581 eleqvrels3 38594 brabsb2 38863 rfovfvd 44015 fsovrfovd 44022 relpeq2 44966 relpeq3 44967 sprsymrelf 47482 sprsymrelfo 47484 upwlkbprop 48054 |
| Copyright terms: Public domain | W3C validator |