| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > breqtrri | Structured version Visualization version GIF version | ||
| Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
| Ref | Expression |
|---|---|
| breqtrr.1 | ⊢ 𝐴𝑅𝐵 |
| breqtrr.2 | ⊢ 𝐶 = 𝐵 |
| Ref | Expression |
|---|---|
| breqtrri | ⊢ 𝐴𝑅𝐶 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | breqtrr.1 | . 2 ⊢ 𝐴𝑅𝐵 | |
| 2 | breqtrr.2 | . . 3 ⊢ 𝐶 = 𝐵 | |
| 3 | 2 | eqcomi 2746 | . 2 ⊢ 𝐵 = 𝐶 |
| 4 | 1, 3 | breqtri 5168 | 1 ⊢ 𝐴𝑅𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 class class class wbr 5143 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 |
| This theorem is referenced by: 3brtr4i 5173 ensn1 9061 1sdom2ALT 9277 dju1p1e2ALT 10215 infmap2 10257 0lt1sr 11135 0le2 12368 2pos 12369 3pos 12371 4pos 12373 5pos 12375 6pos 12376 7pos 12377 8pos 12378 9pos 12379 1lt2 12437 2lt3 12438 3lt4 12440 4lt5 12443 5lt6 12447 6lt7 12452 7lt8 12458 8lt9 12465 numltc 12759 declti 12771 xlemul1a 13330 sqge0i 14227 faclbnd2 14330 cats1fv 14898 ege2le3 16126 cos2bnd 16224 3dvdsdec 16369 n2dvdsm1 16406 sumeven 16424 divalglem2 16432 pockthi 16945 dec2dvds 17101 prmlem1 17145 prmlem2 17157 1259prm 17173 2503prm 17177 4001prm 17182 2strstr1OLD 17271 vitalilem5 25647 dveflem 26017 tangtx 26547 sinq12ge0 26550 logi 26629 cxpge0 26725 asin1 26937 birthday 26997 lgamgulmlem4 27075 ppiub 27248 bposlem7 27334 lgsdir2lem2 27370 n0scut 28338 pthdlem2 29788 ex-fl 30466 ex-ind-dvds 30480 siilem2 30871 normlem6 31134 normlem7 31135 cm2mi 31645 pjnormi 31740 unierri 32123 dp2lt10 32866 dpgti 32888 pfx1s2 32923 cyc2fv2 33142 cyc3fv3 33159 hgt750lemd 34663 hgt750lem 34666 hgt750lem2 34667 hgt750leme 34673 cnndvlem1 36538 taupi 37324 poimirlem25 37652 poimirlem26 37653 poimirlem27 37654 poimirlem28 37655 ftc1anclem5 37704 fdc 37752 lcmineqlem23 42052 3lexlogpow2ineq2 42060 pellfundgt1 42894 jm2.27dlem2 43022 stoweidlem13 46028 sqwvfoura 46243 sqwvfourb 46244 fourierswlem 46245 tworepnotupword 46901 m1modnep2mod 47354 41prothprm 47606 tgblthelfgott 47802 tgoldbachlt 47803 nnlog2ge0lt1 48487 1aryenefmnd 48567 ackval42 48617 |
| Copyright terms: Public domain | W3C validator |