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 4590 | . 2 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) |
4 | 1, 3 | mpbir 220 | 1 ⊢ 𝐴𝑅𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 class class class wbr 4583 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 |
This theorem is referenced by: eqbrtrri 4606 3brtr4i 4613 infxpenc2 8728 pm110.643 8882 pwsdompw 8909 r1om 8949 aleph1 9272 canthp1lem1 9353 pwxpndom2 9366 neg1lt0 11004 halflt1 11127 3halfnz 11332 declei 11418 numlti 11421 sqlecan 12833 discr 12863 faclbnd3 12941 hashunlei 13072 hashge2el2dif 13117 geo2lim 14445 0.999... 14451 0.999...OLD 14452 geoihalfsum 14453 cos2bnd 14757 sin4lt0 14764 eirrlem 14771 rpnnen2lem3 14784 rpnnen2lem9 14790 aleph1re 14813 1nprm 15230 strle2 15801 strle3 15802 1strstr 15805 2strstr 15809 rngstr 15823 srngfn 15831 lmodstr 15840 ipsstr 15847 phlstr 15857 topgrpstr 15865 otpsstr 15874 otpsstrOLD 15878 odrngstr 15889 imasvalstr 15935 0frgp 18015 cnfldstr 19569 zlmlem 19684 tnglem 22254 iscmet3lem3 22896 mbfimaopnlem 23228 mbfsup 23237 mbfi1fseqlem6 23293 aalioulem3 23893 aaliou3lem3 23903 dvradcnv 23979 asin1 24421 log2cnv 24471 log2tlbnd 24472 mule1 24674 bposlem5 24813 bposlem8 24816 zabsle1 24821 trkgstr 25143 0pth 26100 ex-fl 26696 blocnilem 27043 norm3difi 27388 norm3adifii 27389 bcsiALT 27420 nmopsetn0 28108 nmfnsetn0 28121 nmopge0 28154 nmfnge0 28170 0bdop 28236 nmcexi 28269 opsqrlem6 28388 locfinref 29236 dya2iocct 29669 signswch 29964 subfaclim 30424 logi 30873 faclim 30885 cnndvlem1 31698 taupilem2 32345 cntotbnd 32765 diophren 36395 algstr 36766 binomcxplemnn0 37570 binomcxplemrat 37571 stirlinglem1 38967 dirkercncflem1 38996 fouriersw 39124 meaiunlelem 39361 evengpoap3 40215 0pth-av 41293 exple2lt6 41939 nnlog2ge0lt1 42158 |
Copyright terms: Public domain | W3C validator |