![]() |
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 4423 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbir 214 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-br 4417 |
This theorem is referenced by: eqbrtrri 4438 3brtr4i 4445 infxpenc2 8479 pm110.643 8633 pwsdompw 8660 r1om 8700 aleph1 9022 canthp1lem1 9103 pwxpndom2 9116 neg1lt0 10744 halflt1 10860 numlti 11104 sqlecan 12413 discr 12441 faclbnd3 12509 hashunlei 12630 hashge2el2dif 12670 geo2lim 13980 0.999... 13986 geoihalfsum 13987 cos2bnd 14291 sin4lt0 14298 eirrlem 14305 rpnnen2lem3 14318 rpnnen2lem9 14324 aleph1re 14346 1nprm 14678 163prm 15145 631prm 15147 strle2 15271 strle3 15272 1strstr 15275 2strstr 15279 rngstr 15293 srngfn 15301 lmodstr 15310 ipsstr 15317 phlstr 15327 topgrpstr 15335 otpsstr 15342 odrngstr 15353 imasvalstr 15399 ipostr 16448 0frgp 17478 cnfldstr 19021 zlmlem 19137 thlle 19309 tnglem 21697 iscmet3lem3 22309 mbfimaopnlem 22660 mbfsup 22669 mbfi1fseqlem6 22727 aalioulem3 23339 aaliou3lem3 23349 dvradcnv 23425 asin1 23869 log2cnv 23919 log2tlbnd 23920 mule1 24124 bposlem5 24265 bposlem8 24268 trkgstr 24541 0pth 25349 ex-fl 25946 blocnilem 26494 norm3difi 26849 norm3adifii 26850 bcsiALT 26881 nmopsetn0 27567 nmfnsetn0 27580 nmopge0 27613 nmfnge0 27629 0bdop 27695 nmcexi 27728 opsqrlem6 27847 locfinref 28717 dya2iocct 29151 signswch 29499 subfaclim 29960 logi 30419 faclim 30431 taupilem2 31768 cntotbnd 32173 diophren 35701 algstr 36088 binomcxplemnn0 36742 binomcxplemrat 36743 stirlinglem1 37974 dirkercncflem1 38003 fouriersw 38133 meaiunlelem 38344 0pth-av 39841 exple2lt6 40422 3halfnz 40590 nnlog2ge0lt1 40650 |
Copyright terms: Public domain | W3C validator |