![]() |
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 2815 | . 2 ⊢ (𝑅 = 𝑆 → (〈𝐴, 𝐵〉 ∈ 𝑅 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
2 | df-br 5146 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
3 | df-br 5146 | . 2 ⊢ (𝐴𝑆𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆) | |
4 | 1, 2, 3 | 3bitr4g 313 | 1 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 〈cop 4631 class class class wbr 5145 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-clel 2803 df-br 5146 |
This theorem is referenced by: breqi 5151 breqd 5156 poeq1 5589 soeq1 5607 freq1 5644 fveq1 6891 foeqcnvco 7305 f1eqcocnv 7306 isoeq2 7321 isoeq3 7322 eqfunresadj 7363 brfvopab 7473 ofreq 7685 supeq3 9484 oieq1 9547 ttrcleq 9744 dcomex 10480 axdc2lem 10481 brdom3 10561 brdom7disj 10564 brdom6disj 10565 dfrtrclrec2 15057 relexpindlem 15062 rtrclind 15064 shftfval 15069 isprs 18316 isdrs 18320 ispos 18333 istos 18437 efglem 19709 frgpuplem 19765 ordtval 23180 utop2nei 24242 utop3cls 24243 isucn2 24271 ucnima 24273 iducn 24275 ex-opab 30361 resspos 32838 acycgr0v 34988 prclisacycgr 34991 satf 35193 cureq 37309 poimirlem31 37364 poimir 37366 cosseq 38136 elrefrels3 38229 elcnvrefrels3 38245 elsymrels3 38264 elsymrels5 38266 eltrrels3 38290 eleqvrels3 38303 brabsb2 38572 rfovfvd 43705 fsovrfovd 43712 sprsymrelf 47102 sprsymrelfo 47104 upwlkbprop 47550 |
Copyright terms: Public domain | W3C validator |