| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3brtr3g | 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 |
|---|---|
| 3brtr3g.1 | ⊢ (𝜑 → 𝐴𝑅𝐵) |
| 3brtr3g.2 | ⊢ 𝐴 = 𝐶 |
| 3brtr3g.3 | ⊢ 𝐵 = 𝐷 |
| Ref | Expression |
|---|---|
| 3brtr3g | ⊢ (𝜑 → 𝐶𝑅𝐷) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3brtr3g.1 | . 2 ⊢ (𝜑 → 𝐴𝑅𝐵) | |
| 2 | 3brtr3g.2 | . . 3 ⊢ 𝐴 = 𝐶 | |
| 3 | 3brtr3g.3 | . . 3 ⊢ 𝐵 = 𝐷 | |
| 4 | 2, 3 | breq12i 5112 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷) |
| 5 | 1, 4 | sylib 221 | 1 ⊢ (𝜑 → 𝐶𝑅𝐷) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 = wceq 1570 class class class wbr 5103 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2732 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2100 df-clab 2739 df-cleq 2752 df-clel 2835 df-rab 3413 df-v 3452 df-dif 3902 df-un 3904 df-ss 3916 df-nul 4280 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 |
| This theorem is used by: eqbrtrrid 5141 breqtrdi 5146 ssenen 9150 adderpq 10966 mulerpq 10967 ltaddnq 10984 ege2le3 16177 omndaddr 20257 ogrpaddltrd 20268 ovolfiniun 25730 dvfsumlem3 26256 basellem9 27326 pnt2 27850 pnt 27851 siilem1 31333 sn-0ne2 43282 |
| Copyright terms: Public domain | W3C validator |