![]() |
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 4692 | . 2 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) |
4 | 1, 3 | mpbir 221 | 1 ⊢ 𝐴𝑅𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 class class class wbr 4685 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 |
This theorem is referenced by: eqbrtrri 4708 3brtr4i 4715 infxpenc2 8883 pm110.643 9037 pwsdompw 9064 r1om 9104 aleph1 9431 canthp1lem1 9512 pwxpndom2 9525 neg1lt0 11165 halflt1 11288 3halfnz 11494 declei 11580 numlti 11583 sqlecan 13011 discr 13041 faclbnd3 13119 hashunlei 13250 hashge2el2dif 13300 geo2lim 14650 0.999... 14656 0.999...OLD 14657 geoihalfsum 14658 cos2bnd 14962 sin4lt0 14969 eirrlem 14976 rpnnen2lem3 14989 rpnnen2lem9 14995 aleph1re 15018 1nprm 15439 strle2 16021 strle3 16022 1strstr 16026 2strstr 16030 rngstr 16047 srngfn 16055 lmodstr 16064 ipsstr 16071 phlstr 16081 topgrpstr 16089 otpsstr 16098 otpsstrOLD 16102 odrngstr 16113 imasvalstr 16159 0frgp 18238 cnfldstr 19796 zlmlem 19913 tnglem 22491 iscmet3lem3 23134 mbfimaopnlem 23467 mbfsup 23476 mbfi1fseqlem6 23532 aalioulem3 24134 aaliou3lem3 24144 dvradcnv 24220 asin1 24666 log2cnv 24716 log2tlbnd 24717 mule1 24919 bposlem5 25058 bposlem8 25061 zabsle1 25066 trkgstr 25388 0pth 27103 ex-fl 27434 blocnilem 27787 norm3difi 28132 norm3adifii 28133 bcsiALT 28164 nmopsetn0 28852 nmfnsetn0 28865 nmopge0 28898 nmfnge0 28914 0bdop 28980 nmcexi 29013 opsqrlem6 29132 dp2lt10 29719 dplti 29741 dpmul4 29750 locfinref 30036 dya2iocct 30470 signswch 30766 hgt750lem 30857 hgt750lem2 30858 subfaclim 31296 logi 31746 faclim 31758 cnndvlem1 32653 taupilem2 33298 cntotbnd 33725 diophren 37694 algstr 38064 binomcxplemnn0 38865 binomcxplemrat 38866 stirlinglem1 40609 dirkercncflem1 40638 fouriersw 40766 meaiunlelem 41003 evengpoap3 42012 exple2lt6 42470 nnlog2ge0lt1 42685 |
Copyright terms: Public domain | W3C validator |