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 5086 | . 2 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) |
4 | 1, 3 | mpbir 230 | 1 ⊢ 𝐴𝑅𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 class class class wbr 5079 |
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 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-ext 2711 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-rab 3075 df-v 3433 df-dif 3895 df-un 3897 df-nul 4263 df-if 4466 df-sn 4568 df-pr 4570 df-op 4574 df-br 5080 |
This theorem is referenced by: eqbrtrri 5102 3brtr4i 5109 infxpenc2 9779 dju1p1e2 9930 pwsdompw 9961 r1om 10001 aleph1 10328 canthp1lem1 10409 neg1lt0 12090 halflt1 12191 3halfnz 12399 declei 12472 numlti 12473 sqlecan 13923 discr 13953 faclbnd3 14004 hashunlei 14138 hashge2el2dif 14192 geo2lim 15585 0.999... 15591 geoihalfsum 15592 cos2bnd 15895 sin4lt0 15902 eirrlem 15911 rpnnen2lem3 15923 rpnnen2lem9 15929 aleph1re 15952 1nprm 16382 strle2 16858 strle3 16859 1strstr 16925 1strstr1 16926 2strstr 16932 2strstr1 16935 rngstr 17006 srngstr 17017 lmodstr 17033 ipsstr 17044 phlstr 17054 topgrpstr 17069 otpsstr 17084 odrngstr 17111 imasvalstr 17160 0frgp 19383 cnfldstr 20597 zlmlemOLD 20717 tnglemOLD 23795 iscmet3lem3 24452 mbfimaopnlem 24817 mbfsup 24826 mbfi1fseqlem6 24883 aalioulem3 25492 aaliou3lem3 25502 dvradcnv 25578 asin1 26042 log2cnv 26092 log2tlbnd 26093 mule1 26295 bposlem5 26434 bposlem8 26437 zabsle1 26442 trkgstr 26803 0pth 28485 ex-fl 28807 blocnilem 29162 norm3difi 29505 norm3adifii 29506 bcsiALT 29537 nmopsetn0 30223 nmfnsetn0 30236 nmopge0 30269 nmfnge0 30285 0bdop 30351 nmcexi 30384 opsqrlem6 30503 dp2lt10 31154 dplti 31175 dpmul4 31184 idlsrgstr 31643 locfinref 31787 dya2iocct 32243 signswch 32536 hgt750lem 32627 hgt750lem2 32628 subfaclim 33146 logi 33696 faclim 33708 cnndvlem1 34713 taupilem2 35489 cntotbnd 35950 60gcd7e1 40010 3lexlogpow5ineq1 40059 aks4d1p1p7 40079 acos1half 40167 diophren 40632 algstr 40999 pr2dom 41113 tr3dom 41114 binomcxplemnn0 41937 binomcxplemrat 41938 stirlinglem1 43586 dirkercncflem1 43615 fouriersw 43743 meaiunlelem 43977 nfermltl2rev 45164 evengpoap3 45220 exple2lt6 45669 nnlog2ge0lt1 45881 |
Copyright terms: Public domain | W3C validator |