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 5029 | . 2 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1542 class class class wbr 5027 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-cleq 2730 df-clel 2811 df-br 5028 |
This theorem is referenced by: f1ompt 6879 isocnv3 7092 brtpos2 7920 brwitnlem 8156 brdifun 8342 omxpenlem 8660 infxpenlem 9506 ltpiord 10380 nqerf 10423 nqerid 10426 ordpinq 10436 ltxrlt 10782 ltxr 12586 trclublem 14437 oduleg 17851 oduposb 17855 meet0 17856 join0 17857 xmeterval 23178 pi1cpbl 23789 ltgov 26535 brbtwn 26837 avril1 28392 axhcompl-zf 28925 hlimadd 29120 hhcmpl 29127 hhcms 29130 hlim0 29162 fcoinvbr 30513 brprop 30597 posrasymb 30809 trleile 30818 isarchi 31005 pstmfval 31410 pstmxmet 31411 lmlim 31461 satfbrsuc 32891 eqfunresadj 33299 slenlt 33588 brtxp 33812 brpprod 33817 brpprod3b 33819 brtxpsd2 33827 brdomain 33865 brrange 33866 brimg 33869 brapply 33870 brsuccf 33873 brrestrict 33881 brub 33886 brlb 33887 colineardim1 33993 broutsideof 34053 fneval 34171 relowlpssretop 35147 phpreu 35373 poimirlem26 35415 brid 36054 eqres 36087 alrmomorn 36102 brabidgaw 36107 brabidga 36108 brxrn 36116 br1cossinres 36177 br1cossxrnres 36178 brnonrel 40726 brcofffn 41171 brco2f1o 41172 brco3f1o 41173 clsneikex 41246 clsneinex 41247 clsneiel1 41248 neicvgmex 41257 neicvgel1 41259 climreeq 42680 xlimres 42888 xlimcl 42889 xlimclim 42891 xlimconst 42892 xlimbr 42894 xlimmnfvlem1 42899 xlimmnfvlem2 42900 xlimpnfvlem1 42903 xlimpnfvlem2 42904 xlimuni 42920 gte-lte 45863 gt-lt 45864 gte-lteh 45865 gt-lth 45866 |
Copyright terms: Public domain | W3C validator |