![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqbrtri | Structured version Visualization version GIF version |
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
Ref | Expression |
---|---|
eqbrtr.1 | ⊢ 𝐴 = 𝐵 |
eqbrtr.2 | ⊢ 𝐵𝑅𝐶 |
Ref | Expression |
---|---|
eqbrtri | ⊢ 𝐴𝑅𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqbrtr.2 | . 2 ⊢ 𝐵𝑅𝐶 | |
2 | eqbrtr.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
3 | 2 | breq1i 5149 | . 2 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) |
4 | 1, 3 | mpbir 230 | 1 ⊢ 𝐴𝑅𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 class class class wbr 5142 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-rab 3428 df-v 3471 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-br 5143 |
This theorem is referenced by: eqbrtrri 5165 3brtr4i 5172 0sdom1dom 9254 1sdom2dom 9263 infxpenc2 10037 dju1p1e2 10188 pwsdompw 10219 r1om 10259 aleph1 10586 canthp1lem1 10667 neg1lt0 12351 halflt1 12452 3halfnz 12663 declei 12735 numlti 12736 sqlecan 14196 discr 14226 faclbnd3 14275 hashunlei 14408 hashge2el2dif 14465 geo2lim 15845 0.999... 15851 geoihalfsum 15852 cos2bnd 16156 sin4lt0 16163 eirrlem 16172 rpnnen2lem3 16184 rpnnen2lem9 16190 aleph1re 16213 1nprm 16641 strle2 17119 strle3 17120 1strstr 17186 1strstr1 17187 2strstr 17193 2strstr1 17196 rngstr 17270 srngstr 17281 lmodstr 17297 ipsstr 17308 phlstr 17318 topgrpstr 17333 otpsstr 17348 odrngstr 17375 imasvalstr 17424 0frgp 19725 cnfldstr 21268 cnfldstrOLD 21283 zlmlemOLD 21430 tnglemOLD 24537 iscmet3lem3 25205 mbfimaopnlem 25571 mbfsup 25580 mbfi1fseqlem6 25637 aalioulem3 26256 aaliou3lem3 26266 dvradcnv 26344 logi 26508 asin1 26813 log2cnv 26863 log2tlbnd 26864 mule1 27067 bposlem5 27208 bposlem8 27211 zabsle1 27216 trkgstr 28235 0pth 29922 ex-fl 30244 blocnilem 30601 norm3difi 30944 norm3adifii 30945 bcsiALT 30976 nmopsetn0 31662 nmfnsetn0 31675 nmopge0 31708 nmfnge0 31724 0bdop 31790 nmcexi 31823 opsqrlem6 31942 dp2lt10 32589 dplti 32610 dpmul4 32619 idlsrgstr 33149 locfinref 33378 dya2iocct 33836 signswch 34129 hgt750lem 34219 hgt750lem2 34220 subfaclim 34734 faclim 35276 cnndvlem1 35948 taupilem2 36737 cntotbnd 37204 60gcd7e1 41413 3lexlogpow5ineq1 41462 aks4d1p1p7 41482 acos1half 42019 diophren 42155 algstr 42523 pr2dom 42880 tr3dom 42881 binomcxplemnn0 43709 binomcxplemrat 43710 stirlinglem1 45385 dirkercncflem1 45414 fouriersw 45542 meaiunlelem 45779 nfermltl2rev 47006 evengpoap3 47062 exple2lt6 47351 nnlog2ge0lt1 47562 |
Copyright terms: Public domain | W3C validator |