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 2677 | . 2 ⊢ (𝑅 = 𝑆 → (〈𝐴, 𝐵〉 ∈ 𝑅 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
2 | df-br 4584 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
3 | df-br 4584 | . 2 ⊢ (𝐴𝑆𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆) | |
4 | 1, 2, 3 | 3bitr4g 302 | 1 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∈ wcel 1977 〈cop 4131 class class class wbr 4583 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-cleq 2603 df-clel 2606 df-br 4584 |
This theorem is referenced by: breqi 4589 breqd 4594 poeq1 4962 soeq1 4978 freq1 5008 fveq1 6102 foeqcnvco 6455 f1eqcocnv 6456 isoeq2 6468 isoeq3 6469 brfvopab 6598 ofreq 6798 supeq3 8238 oieq1 8300 dcomex 9152 axdc2lem 9153 brdom3 9231 brdom7disj 9234 brdom6disj 9235 dfrtrclrec2 13645 rtrclreclem3 13648 relexpindlem 13651 rtrclind 13653 shftfval 13658 isprs 16753 isdrs 16757 ispos 16770 istos 16858 efglem 17952 frgpuplem 18008 ordtval 20803 utop2nei 21864 utop3cls 21865 isucn2 21893 ucnima 21895 iducn 21897 ex-opab 26681 resspos 28990 cureq 32555 poimirlem31 32610 poimir 32612 brabsb2 33165 rfovfvd 37316 fsovrfovd 37323 wlkbProp 40817 |
Copyright terms: Public domain | W3C validator |