![]() |
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 4969 | . 2 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) |
4 | 1, 3 | mpbir 232 | 1 ⊢ 𝐴𝑅𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 class class class wbr 4962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-br 4963 |
This theorem is referenced by: eqbrtrri 4985 3brtr4i 4992 infxpenc2 9294 dju1p1e2 9445 pwsdompw 9472 r1om 9512 aleph1 9839 canthp1lem1 9920 neg1lt0 11602 halflt1 11703 3halfnz 11910 declei 11983 numlti 11984 sqlecan 13421 discr 13451 faclbnd3 13502 hashunlei 13634 hashge2el2dif 13684 geo2lim 15064 0.999... 15070 geoihalfsum 15071 cos2bnd 15374 sin4lt0 15381 eirrlem 15390 rpnnen2lem3 15402 rpnnen2lem9 15408 aleph1re 15431 1nprm 15852 strle2 16422 strle3 16423 1strstr 16427 2strstr 16431 rngstr 16448 srngstr 16456 lmodstr 16465 ipsstr 16472 phlstr 16482 topgrpstr 16490 otpsstr 16497 odrngstr 16508 imasvalstr 16554 0frgp 18632 cnfldstr 20229 zlmlem 20346 tnglem 22932 iscmet3lem3 23576 mbfimaopnlem 23939 mbfsup 23948 mbfi1fseqlem6 24004 aalioulem3 24606 aaliou3lem3 24616 dvradcnv 24692 asin1 25153 log2cnv 25204 log2tlbnd 25205 mule1 25407 bposlem5 25546 bposlem8 25549 zabsle1 25554 trkgstr 25912 0pth 27591 ex-fl 27918 blocnilem 28272 norm3difi 28615 norm3adifii 28616 bcsiALT 28647 nmopsetn0 29333 nmfnsetn0 29346 nmopge0 29379 nmfnge0 29395 0bdop 29461 nmcexi 29494 opsqrlem6 29613 dp2lt10 30244 dplti 30265 dpmul4 30274 locfinref 30722 dya2iocct 31155 signswch 31448 hgt750lem 31539 hgt750lem2 31540 subfaclim 32043 logi 32574 faclim 32586 cnndvlem1 33485 taupilem2 34134 cntotbnd 34606 diophren 38895 algstr 39262 pr2dom 39378 tr3dom 39379 binomcxplemnn0 40219 binomcxplemrat 40220 stirlinglem1 41901 dirkercncflem1 41930 fouriersw 42058 meaiunlelem 42292 nfermltl2rev 43390 evengpoap3 43446 exple2lt6 43892 nnlog2ge0lt1 44107 |
Copyright terms: Public domain | W3C validator |