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

Theorem breq12 4444
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 4442 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
2 breq2 4443 . 2  |-  ( C  =  D  ->  ( B R C  <->  B R D ) )
31, 2sylan9bb 697 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1398   class class class wbr 4439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440
This theorem is referenced by:  breq12i  4448  breq12d  4452  breqan12d  4454  posn  5057  isopolem  6216  poxp  6885  soxp  6886  fnse  6890  isprmpt2  6945  ecopover  7407  canth2g  7664  infxpen  8383  sornom  8648  dcomex  8818  zorn2lem6  8872  brdom6disj  8901  fpwwe2  9010  rankcf  9144  ltresr  9506  ltxrlt  9644  wloglei  10081  ltxr  11327  xrltnr  11333  xrltnsym  11346  xrlttri  11348  xrlttr  11349  brfi1uzind  12519  f1olecpbl  15019  isfull  15401  isfth  15405  prslem  15762  pslem  16038  dirtr  16068  xrsdsval  18660  dvcvx  22590  axcontlem9  24480  iscusgra  24661  sizeusglecusg  24691  iswlkon  24739  istrlon  24748  ispth  24775  isspth  24776  ispthon  24783  0pthonv  24788  isspthon  24790  1pthon2v  24800  2pthon3v  24811  usg2wlk  24822  usg2wlkon  24823  constr3cyclpe  24868  3v3e3cycl2  24869  isclwlk0  24959  isrusgra  25132  iseupa  25170  dfrel4  27671  2sqmo  27874  mclsppslem  29210  dfpo2  29428  fununiq  29443  elfix2  29785  monotoddzzfi  31120  wlkc  32741  lindepsnlininds  33326
  Copyright terms: Public domain W3C validator