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 2828 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | breqtri 5082 | 1 ⊢ 𝐴𝑅𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1531 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 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-rab 3145 df-v 3495 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5058 |
This theorem is referenced by: 3brtr4i 5087 ensn1 8565 1sdom2 8709 dju1p1e2ALT 9592 infmap2 9632 0lt1sr 10509 0le2 11731 2pos 11732 3pos 11734 4pos 11736 5pos 11738 6pos 11739 7pos 11740 8pos 11741 9pos 11742 1lt2 11800 2lt3 11801 3lt4 11803 4lt5 11806 5lt6 11810 6lt7 11815 7lt8 11821 8lt9 11828 nn0le2xi 11943 numltc 12116 declti 12128 xlemul1a 12673 sqge0i 13543 faclbnd2 13643 cats1fv 14213 ege2le3 15435 cos2bnd 15533 3dvdsdec 15673 n2dvdsm1 15711 n2dvds3OLD 15714 sumeven 15730 divalglem2 15738 pockthi 16235 dec2dvds 16391 prmlem1 16433 prmlem2 16445 1259prm 16461 2503prm 16465 4001prm 16470 2strstr1 16597 vitalilem5 24205 dveflem 24568 tangtx 25083 sinq12ge0 25086 cxpge0 25258 asin1 25464 birthday 25524 lgamgulmlem4 25601 ppiub 25772 bposlem7 25858 lgsdir2lem2 25894 pthdlem2 27541 ex-fl 28218 ex-ind-dvds 28232 siilem2 28621 normlem6 28884 normlem7 28885 cm2mi 29395 pjnormi 29490 unierri 29873 dp2lt10 30553 dpgti 30575 pfx1s2 30608 cyc2fv2 30757 cyc3fv3 30774 hgt750lemd 31912 hgt750lem 31915 hgt750lem2 31916 hgt750leme 31922 logi 32959 cnndvlem1 33869 taupi 34596 poimirlem25 34909 poimirlem26 34910 poimirlem27 34911 poimirlem28 34912 ftc1anclem5 34963 fdc 35012 pellfundgt1 39471 jm2.27dlem2 39598 stoweidlem13 42289 sqwvfoura 42504 sqwvfourb 42505 fourierswlem 42506 41prothprm 43775 tgblthelfgott 43971 tgoldbachlt 43972 nnlog2ge0lt1 44617 |
Copyright terms: Public domain | W3C validator |