![]() |
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 4964 | . 2 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1522 class class class wbr 4962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 df-cleq 2788 df-clel 2863 df-br 4963 |
This theorem is referenced by: f1ompt 6738 isocnv3 6948 brtpos2 7749 brwitnlem 7983 brdifun 8168 omxpenlem 8465 infxpenlem 9285 ltpiord 10155 nqerf 10198 nqerid 10201 ordpinq 10211 ltxrlt 10558 ltxr 12360 trclublem 14189 oduleg 17571 oduposb 17575 meet0 17576 join0 17577 xmeterval 22725 pi1cpbl 23331 ltgov 26065 brbtwn 26368 avril1 27933 axhcompl-zf 28466 hlimadd 28661 hhcmpl 28668 hhcms 28671 hlim0 28703 fcoinvbr 30048 brprop 30121 posrasymb 30318 trleile 30327 isarchi 30449 pstmfval 30753 pstmxmet 30754 lmlim 30807 satfbrsuc 32221 eqfunresadj 32612 slenlt 32840 brtxp 32950 brpprod 32955 brpprod3b 32957 brtxpsd2 32965 brdomain 33003 brrange 33004 brimg 33007 brapply 33008 brsuccf 33011 brrestrict 33019 brub 33024 brlb 33025 colineardim1 33131 broutsideof 33191 fneval 33309 relowlpssretop 34176 phpreu 34407 poimirlem26 34449 brid 35096 eqres 35129 alrmomorn 35144 brabidga 35149 brxrn 35157 br1cossinres 35218 br1cossxrnres 35219 brnonrel 39434 brcofffn 39866 brco2f1o 39867 brco3f1o 39868 clsneikex 39941 clsneinex 39942 clsneiel1 39943 neicvgmex 39952 neicvgel1 39954 climreeq 41436 xlimres 41644 xlimcl 41645 xlimclim 41647 xlimconst 41648 xlimbr 41650 xlimmnfvlem1 41655 xlimmnfvlem2 41656 xlimpnfvlem1 41659 xlimpnfvlem2 41660 xlimuni 41676 gte-lte 44303 gt-lt 44304 gte-lteh 44305 gt-lth 44306 |
Copyright terms: Public domain | W3C validator |