|   | 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 234 | 1 ⊢ (𝜑 → 𝐶𝑅𝐷) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1539 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 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-br 5143 | 
| This theorem is referenced by: eqbrtrid 5177 enrefnn 9088 enpr2dOLD 9091 limensuci 9194 infensuc 9196 djuen 10211 djudom1 10224 rlimneg 15684 isumsup2 15883 crth 16816 4sqlem6 16982 gzrngunit 21452 matgsum 22444 ovolunlem1a 25532 ovolfiniun 25537 ioombl1lem1 25594 ioombl1lem4 25597 iblss 25841 itgle 25846 dvfsumlem3 26070 emcllem6 27045 gausslemma2dlem0f 27406 gausslemma2dlem0g 27407 pntpbnd1a 27630 ostth2lem4 27681 noinfbnd2lem1 27776 omsmon 34301 itg2gt0cn 37683 dalem-cly 39674 dalem10 39676 fourierdlem103 46229 fourierdlem104 46230 | 
| Copyright terms: Public domain | W3C validator |