![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3brtr4g | Structured version Visualization version GIF 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 5151 | . 2 ⊢ (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵) |
5 | 1, 4 | sylibr 233 | 1 ⊢ (𝜑 → 𝐶𝑅𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 class class class wbr 5142 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4320 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-br 5143 |
This theorem is referenced by: eqbrtrid 5177 enrefnn 9032 enpr2dOLD 9035 limensuci 9138 infensuc 9140 djuen 10148 djudom1 10161 rlimneg 15577 isumsup2 15776 crth 16695 4sqlem6 16860 gzrngunit 20947 matgsum 21870 ovolunlem1a 24944 ovolfiniun 24949 ioombl1lem1 25006 ioombl1lem4 25009 iblss 25253 itgle 25258 dvfsumlem3 25476 emcllem6 26434 gausslemma2dlem0f 26793 gausslemma2dlem0g 26794 pntpbnd1a 27017 ostth2lem4 27068 noinfbnd2lem1 27162 omsmon 33192 itg2gt0cn 36411 dalem-cly 38411 dalem10 38413 fourierdlem103 44762 fourierdlem104 44763 |
Copyright terms: Public domain | W3C validator |