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

Theorem breq12 4217
Description: Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
Assertion
Ref Expression
breq12  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )

Proof of Theorem breq12
StepHypRef Expression
1 breq1 4215 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
2 breq2 4216 . 2  |-  ( C  =  D  ->  ( B R C  <->  B R D ) )
31, 2sylan9bb 681 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652   class class class wbr 4212
This theorem is referenced by:  breq12i  4221  breq12d  4225  breqan12d  4227  posn  4946  isopolem  6065  poxp  6458  soxp  6459  fnse  6463  isprmpt2  6477  ecopover  7008  canth2g  7261  infxpen  7896  sornom  8157  dcomex  8327  zorn2lem6  8381  brdom6disj  8410  fpwwe2  8518  rankcf  8652  ltresr  9015  ltxrlt  9146  wloglei  9559  ltxr  10715  xrltnr  10720  xrltnsym  10730  xrlttri  10732  xrlttr  10733  brfi1uzind  11715  f1olecpbl  13752  isfull  14107  isfth  14111  prslem  14388  pslem  14638  dirtr  14681  xrsdsval  16742  dvcvx  19904  iscusgra  21465  sizeusglecusg  21495  iswlkon  21531  istrlon  21541  ispth  21568  isspth  21569  ispthon  21576  0pthonv  21581  isspthon  21583  1pthon2v  21593  2pthon3v  21604  constr3cyclpe  21650  3v3e3cycl2  21651  iseupa  21687  dfrel4  24034  dfpo2  25378  fununiq  25394  elfix2  25749  axcontlem9  25911  monotoddzzfi  27005  usg2wlk  28319  usg2wlkon  28320  isrusgra  28370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator