![]() |
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 5150 | . 2 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1540 class class class wbr 5148 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-cleq 2723 df-clel 2809 df-br 5149 |
This theorem is referenced by: f1ompt 7112 isocnv3 7332 eqfunresadj 7360 brtpos2 8223 brwitnlem 8513 brdifun 8738 omxpenlem 9079 infxpenlem 10014 ltpiord 10888 nqerf 10931 nqerid 10934 ordpinq 10944 ltxrlt 11291 ltxr 13102 trclublem 14949 oduleg 18250 oduposb 18289 join0 18365 meet0 18366 xmeterval 24171 pi1cpbl 24804 slenlt 27506 ltgov 28130 brbtwn 28439 avril1 29998 axhcompl-zf 30533 hlimadd 30728 hhcmpl 30735 hhcms 30738 hlim0 30770 fcoinvbr 32118 brprop 32201 posrasymb 32417 trleile 32423 isarchi 32613 pstmfval 33189 pstmxmet 33190 lmlim 33240 satfbrsuc 34670 brtxp 35171 brpprod 35176 brpprod3b 35178 brtxpsd2 35186 brdomain 35224 brrange 35225 brimg 35228 brapply 35229 brsuccf 35232 brrestrict 35240 brub 35245 brlb 35246 colineardim1 35352 broutsideof 35412 fneval 35553 relowlpssretop 36561 phpreu 36788 poimirlem26 36830 br1cnvres 37453 brid 37491 eqres 37525 alrmomorn 37543 brabidgaw 37550 brabidga 37551 brxrn 37560 br1cossinres 37633 br1cossxrnres 37634 brnonrel 42655 brcofffn 43097 brco2f1o 43098 brco3f1o 43099 clsneikex 43172 clsneinex 43173 clsneiel1 43174 neicvgmex 43183 neicvgel1 43185 climreeq 44640 xlimres 44848 xlimcl 44849 xlimclim 44851 xlimconst 44852 xlimbr 44854 xlimmnfvlem1 44859 xlimmnfvlem2 44860 xlimpnfvlem1 44863 xlimpnfvlem2 44864 xlimuni 44880 gte-lte 47869 gt-lt 47870 gte-lteh 47871 gt-lth 47872 |
Copyright terms: Public domain | W3C validator |