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

Theorem breq12 5057
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 5055 . 2 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
2 breq2 5056 . 2 (𝐶 = 𝐷 → (𝐵𝑅𝐶𝐵𝑅𝐷))
31, 2sylan9bb 513 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538   class class class wbr 5052
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-sn 4551  df-pr 4553  df-op 4557  df-br 5053
This theorem is referenced by:  breq12i  5061  breq12d  5065  breqan12d  5068  rbropapd  5436  posn  5624  dfrel4  6035  isopolem  7091  poxp  7818  soxp  7819  fnse  7823  ecopover  8397  canth2g  8668  infxpen  9438  sornom  9697  dcomex  9867  zorn2lem6  9921  brdom6disj  9952  fpwwe2  10063  rankcf  10197  ltresr  10560  ltxrlt  10709  wloglei  11170  ltxr  12507  xrltnr  12511  xrltnsym  12527  xrlttri  12529  xrlttr  12530  brfi1uzind  13861  brfi1indALT  13863  f1olecpbl  16800  isfull  17180  isfth  17184  prslem  17541  pslem  17816  dirtr  17846  xrsdsval  20589  dvcvx  24626  2sqmo  26024  2sqreultblem  26035  2sqreunnltblem  26038  2sqreuopb  26055  axcontlem9  26769  isrusgr  27354  wlk2f  27422  istrlson  27499  upgrwlkdvspth  27531  ispthson  27534  isspthson  27535  crctcshwlk  27611  crctcsh  27613  2pthon3v  27732  umgr2wlk  27738  0pthonv  27917  1pthon2v  27941  uhgr3cyclex  27970  brfinext  31103  mclsppslem  32887  dfpo2  33048  fununiq  33069  slerec  33334  elfix2  33422  poimirlem10  35012  poimirlem11  35013  factwoffsmonot  39325  monotoddzzfi  39799  or2expropbi  43552  dfatcolem  43737  sprsymrelfolem2  43936  poprelb  43967  lindepsnlininds  44787
  Copyright terms: Public domain W3C validator