Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqbrtrri | Structured version Visualization version GIF version |
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
Ref | Expression |
---|---|
eqbrtrr.1 | ⊢ 𝐴 = 𝐵 |
eqbrtrr.2 | ⊢ 𝐴𝑅𝐶 |
Ref | Expression |
---|---|
eqbrtrri | ⊢ 𝐵𝑅𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqbrtrr.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | 1 | eqcomi 2827 | . 2 ⊢ 𝐵 = 𝐴 |
3 | eqbrtrr.2 | . 2 ⊢ 𝐴𝑅𝐶 | |
4 | 2, 3 | eqbrtri 5078 | 1 ⊢ 𝐵𝑅𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 class class class wbr 5057 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 |
This theorem is referenced by: 3brtr3i 5086 expnass 13558 faclbnd4lem1 13641 sqrt2gt1lt2 14622 cos1bnd 15528 cos2bnd 15529 2strstr1 16593 prdsvalstr 16714 ovolre 24053 pigt3 25030 pige3ALT 25032 atan1 25433 log2ublem1 25451 sqrtlim 25477 bposlem8 25794 chebbnd1 25975 norm-ii-i 28841 nmopadji 29794 unierri 29808 ballotlem2 31645 hgt750lemd 31818 hgt750lem 31821 stoweidlem26 42188 wallispilem5 42231 |
Copyright terms: Public domain | W3C validator |