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

Theorem breq12 4295
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 4293 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
2 breq2 4294 . 2  |-  ( C  =  D  ->  ( B R C  <->  B R D ) )
31, 2sylan9bb 699 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369   class class class wbr 4290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-op 3882  df-br 4291
This theorem is referenced by:  breq12i  4299  breq12d  4303  breqan12d  4305  posn  4905  isopolem  6034  poxp  6682  soxp  6683  fnse  6687  isprmpt2  6741  ecopover  7202  canth2g  7463  infxpen  8179  sornom  8444  dcomex  8614  zorn2lem6  8668  brdom6disj  8697  fpwwe2  8808  rankcf  8942  ltresr  9305  ltxrlt  9443  wloglei  9870  ltxr  11093  xrltnr  11099  xrltnsym  11112  xrlttri  11114  xrlttr  11115  brfi1uzind  12217  f1olecpbl  14463  isfull  14818  isfth  14822  prslem  15099  pslem  15374  dirtr  15404  xrsdsval  17855  dvcvx  21490  axcontlem9  23216  iscusgra  23362  sizeusglecusg  23392  iswlkon  23428  istrlon  23438  ispth  23465  isspth  23466  ispthon  23473  0pthonv  23478  isspthon  23480  1pthon2v  23490  2pthon3v  23501  constr3cyclpe  23547  3v3e3cycl2  23548  iseupa  23584  dfrel4  25935  dfpo2  27563  fununiq  27579  elfix2  27933  monotoddzzfi  29280  wlkc  30290  usg2wlk  30306  usg2wlkon  30307  isclwlk0  30416  isrusgra  30541  lindepsnlininds  30983
  Copyright terms: Public domain W3C validator