Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqbrtri | Structured version Visualization version Unicode 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 4660 | . 2 |
4 | 1, 3 | mpbir 221 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wceq 1483 class class class wbr 4653 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 |
This theorem is referenced by: eqbrtrri 4676 3brtr4i 4683 infxpenc2 8845 pm110.643 8999 pwsdompw 9026 r1om 9066 aleph1 9393 canthp1lem1 9474 pwxpndom2 9487 neg1lt0 11127 halflt1 11250 3halfnz 11456 declei 11542 numlti 11545 sqlecan 12971 discr 13001 faclbnd3 13079 hashunlei 13212 hashge2el2dif 13262 geo2lim 14606 0.999... 14612 0.999...OLD 14613 geoihalfsum 14614 cos2bnd 14918 sin4lt0 14925 eirrlem 14932 rpnnen2lem3 14945 rpnnen2lem9 14951 aleph1re 14974 1nprm 15392 strle2 15974 strle3 15975 1strstr 15979 2strstr 15983 rngstr 16000 srngfn 16008 lmodstr 16017 ipsstr 16024 phlstr 16034 topgrpstr 16042 otpsstr 16051 otpsstrOLD 16055 odrngstr 16066 imasvalstr 16112 0frgp 18192 cnfldstr 19748 zlmlem 19865 tnglem 22444 iscmet3lem3 23088 mbfimaopnlem 23422 mbfsup 23431 mbfi1fseqlem6 23487 aalioulem3 24089 aaliou3lem3 24099 dvradcnv 24175 asin1 24621 log2cnv 24671 log2tlbnd 24672 mule1 24874 bposlem5 25013 bposlem8 25016 zabsle1 25021 trkgstr 25343 0pth 26986 ex-fl 27304 blocnilem 27659 norm3difi 28004 norm3adifii 28005 bcsiALT 28036 nmopsetn0 28724 nmfnsetn0 28737 nmopge0 28770 nmfnge0 28786 0bdop 28852 nmcexi 28885 opsqrlem6 29004 dp2lt10 29591 dplti 29613 dpmul4 29622 locfinref 29908 dya2iocct 30342 signswch 30638 hgt750lem 30729 hgt750lem2 30730 subfaclim 31170 logi 31620 faclim 31632 cnndvlem1 32528 taupilem2 33168 cntotbnd 33595 diophren 37377 algstr 37747 binomcxplemnn0 38548 binomcxplemrat 38549 stirlinglem1 40291 dirkercncflem1 40320 fouriersw 40448 meaiunlelem 40685 evengpoap3 41687 exple2lt6 42145 nnlog2ge0lt1 42360 |
Copyright terms: Public domain | W3C validator |