| 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 5145 | . 2 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = wceq 1540 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: f1ompt 7131 isocnv3 7352 eqfunresadj 7380 brtpos2 8257 brwitnlem 8545 brdifun 8775 omxpenlem 9113 infxpenlem 10053 ltpiord 10927 nqerf 10970 nqerid 10973 ordpinq 10983 ltxrlt 11331 ltxr 13157 trclublem 15034 oduleg 18335 oduposb 18374 join0 18450 meet0 18451 xmeterval 24442 pi1cpbl 25077 slenlt 27797 ltgov 28605 brbtwn 28914 avril1 30482 axhcompl-zf 31017 hlimadd 31212 hhcmpl 31219 hhcms 31222 hlim0 31254 fcoinvbr 32618 brprop 32706 posrasymb 32955 trleile 32961 isarchi 33189 pstmfval 33895 pstmxmet 33896 lmlim 33946 satfbrsuc 35371 brtxp 35881 brpprod 35886 brpprod3b 35888 brtxpsd2 35896 brdomain 35934 brrange 35935 brimg 35938 brapply 35939 brsuccf 35942 brrestrict 35950 brub 35955 brlb 35956 colineardim1 36062 broutsideof 36122 fneval 36353 relowlpssretop 37365 phpreu 37611 poimirlem26 37653 br1cnvres 38270 brid 38307 eqres 38341 alrmomorn 38359 brabidgaw 38366 brabidga 38367 brxrn 38375 br1cossinres 38448 br1cossxrnres 38449 brnonrel 43602 brcofffn 44044 brco2f1o 44045 brco3f1o 44046 clsneikex 44119 clsneinex 44120 clsneiel1 44121 neicvgmex 44130 neicvgel1 44132 climreeq 45628 xlimres 45836 xlimcl 45837 xlimclim 45839 xlimconst 45840 xlimbr 45842 xlimmnfvlem1 45847 xlimmnfvlem2 45848 xlimpnfvlem1 45851 xlimpnfvlem2 45852 xlimuni 45868 gte-lte 49243 gt-lt 49244 gte-lteh 49245 gt-lth 49246 |
| Copyright terms: Public domain | W3C validator |