![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3brtr4g | Structured version Visualization version Unicode version |
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
Ref | Expression |
---|---|
3brtr4g.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3brtr4g.2 |
![]() ![]() ![]() ![]() |
3brtr4g.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3brtr4g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3brtr4g.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3brtr4g.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 3brtr4g.3 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | breq12i 4411 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | sylibr 216 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-rab 2746 df-v 3047 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-sn 3969 df-pr 3971 df-op 3975 df-br 4403 |
This theorem is referenced by: syl5eqbr 4436 limensuci 7748 infensuc 7750 rlimneg 13710 isumsup2 13904 crt 14726 4sqlem6 14887 gzrngunit 19033 matgsum 19462 ovolunlem1a 22449 ovolfiniun 22454 ioombl1lem1 22511 ioombl1lem4 22514 iblss 22762 itgle 22767 dvfsumlem3 22980 emcllem6 23926 pntpbnd1a 24423 ostth2lem4 24474 omsmon 29126 omsmonOLD 29130 itg2gt0cn 31997 dalem-cly 33236 dalem10 33238 fourierdlem103 38073 fourierdlem104 38074 |
Copyright terms: Public domain | W3C validator |