MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breq12 Structured version   Visualization version   GIF version

Theorem breq12 5063
Description: Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
Assertion
Ref Expression
breq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))

Proof of Theorem breq12
StepHypRef Expression
1 breq1 5061 . 2 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
2 breq2 5062 . 2 (𝐶 = 𝐷 → (𝐵𝑅𝐶𝐵𝑅𝐷))
31, 2sylan9bb 510 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528   class class class wbr 5058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059
This theorem is referenced by:  breq12i  5067  breq12d  5071  breqan12d  5074  rbropapd  5441  posn  5631  dfrel4  6042  isopolem  7087  poxp  7813  soxp  7814  fnse  7818  ecopover  8391  canth2g  8660  infxpen  9429  sornom  9688  dcomex  9858  zorn2lem6  9912  brdom6disj  9943  fpwwe2  10054  rankcf  10188  ltresr  10551  ltxrlt  10700  wloglei  11161  ltxr  12500  xrltnr  12504  xrltnsym  12520  xrlttri  12522  xrlttr  12523  brfi1uzind  13846  brfi1indALT  13848  f1olecpbl  16790  isfull  17170  isfth  17174  prslem  17531  pslem  17806  dirtr  17836  xrsdsval  20519  dvcvx  24546  2sqmo  25941  2sqreultblem  25952  2sqreunnltblem  25955  2sqreuopb  25972  axcontlem9  26686  isrusgr  27271  wlk2f  27339  istrlson  27416  upgrwlkdvspth  27448  ispthson  27451  isspthson  27452  crctcshwlk  27528  crctcsh  27530  2pthon3v  27650  umgr2wlk  27656  0pthonv  27836  1pthon2v  27860  uhgr3cyclex  27889  brfinext  30943  mclsppslem  32728  dfpo2  32889  fununiq  32910  slerec  33175  elfix2  33263  poimirlem10  34784  poimirlem11  34785  monotoddzzfi  39419  or2expropbi  43150  dfatcolem  43335  sprsymrelfolem2  43502  poprelb  43533  lindepsnlininds  44405
  Copyright terms: Public domain W3C validator