Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > breqi | Structured version Visualization version GIF version |
Description: Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.) |
Ref | Expression |
---|---|
breqi.1 | ⊢ 𝑅 = 𝑆 |
Ref | Expression |
---|---|
breqi | ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breqi.1 | . 2 ⊢ 𝑅 = 𝑆 | |
2 | breq 5076 | . 2 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1539 class class class wbr 5074 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-cleq 2730 df-clel 2816 df-br 5075 |
This theorem is referenced by: f1ompt 6985 isocnv3 7203 brtpos2 8048 brwitnlem 8337 brdifun 8527 omxpenlem 8860 infxpenlem 9769 ltpiord 10643 nqerf 10686 nqerid 10689 ordpinq 10699 ltxrlt 11045 ltxr 12851 trclublem 14706 oduleg 18008 oduposb 18047 join0 18123 meet0 18124 xmeterval 23585 pi1cpbl 24207 ltgov 26958 brbtwn 27267 avril1 28827 axhcompl-zf 29360 hlimadd 29555 hhcmpl 29562 hhcms 29565 hlim0 29597 fcoinvbr 30947 brprop 31030 posrasymb 31243 trleile 31249 isarchi 31436 pstmfval 31846 pstmxmet 31847 lmlim 31897 satfbrsuc 33328 eqfunresadj 33735 slenlt 33955 brtxp 34182 brpprod 34187 brpprod3b 34189 brtxpsd2 34197 brdomain 34235 brrange 34236 brimg 34239 brapply 34240 brsuccf 34243 brrestrict 34251 brub 34256 brlb 34257 colineardim1 34363 broutsideof 34423 fneval 34541 relowlpssretop 35535 phpreu 35761 poimirlem26 35803 brid 36442 eqres 36475 alrmomorn 36490 brabidgaw 36495 brabidga 36496 brxrn 36504 br1cossinres 36565 br1cossxrnres 36566 brnonrel 41197 brcofffn 41641 brco2f1o 41642 brco3f1o 41643 clsneikex 41716 clsneinex 41717 clsneiel1 41718 neicvgmex 41727 neicvgel1 41729 climreeq 43154 xlimres 43362 xlimcl 43363 xlimclim 43365 xlimconst 43366 xlimbr 43368 xlimmnfvlem1 43373 xlimmnfvlem2 43374 xlimpnfvlem1 43377 xlimpnfvlem2 43378 xlimuni 43394 gte-lte 46426 gt-lt 46427 gte-lteh 46428 gt-lth 46429 |
Copyright terms: Public domain | W3C validator |