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

Theorem breq12 4425
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 4423 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
2 breq2 4424 . 2  |-  ( C  =  D  ->  ( B R C  <->  B R D ) )
31, 2sylan9bb 704 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   class class class wbr 4420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421
This theorem is referenced by:  breq12i  4429  breq12d  4433  breqan12d  4436  posn  4919  isopolem  6248  poxp  6916  soxp  6917  fnse  6921  isprmpt2  6976  ecopover  7472  canth2g  7729  infxpen  8447  sornom  8708  dcomex  8878  zorn2lem6  8932  brdom6disj  8961  fpwwe2  9069  rankcf  9203  ltresr  9565  ltxrlt  9705  wloglei  10147  ltxr  11416  xrltnr  11422  xrltnsym  11437  xrlttri  11439  xrlttr  11440  brfi1uzind  12647  f1olecpbl  15421  isfull  15803  isfth  15807  prslem  16164  pslem  16440  dirtr  16470  xrsdsval  19000  dvcvx  22959  axcontlem9  24989  iscusgra  25170  sizeusglecusg  25200  iswlkon  25248  istrlon  25257  ispth  25284  isspth  25285  ispthon  25292  0pthonv  25297  isspthon  25299  1pthon2v  25309  2pthon3v  25320  usg2wlk  25331  usg2wlkon  25332  constr3cyclpe  25377  3v3e3cycl2  25378  isclwlk0  25468  isrusgra  25641  iseupa  25679  dfrel4  28198  2sqmo  28405  mclsppslem  30217  dfpo2  30390  fununiq  30405  elfix2  30664  poimirlem10  31864  poimirlem11  31865  monotoddzzfi  35710  wlkc  38936  lindepsnlininds  39519
  Copyright terms: Public domain W3C validator