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

Theorem breq12 4457
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 4455 . 2
2 breq2 4456 . 2
31, 2sylan9bb 699 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395   class class class wbr 4452
This theorem is referenced by:  breq12i  4461  breq12d  4465  breqan12d  4467  posn  5073  isopolem  6241  poxp  6912  soxp  6913  fnse  6917  isprmpt2  6972  ecopover  7434  canth2g  7691  infxpen  8413  sornom  8678  dcomex  8848  zorn2lem6  8902  brdom6disj  8931  fpwwe2  9042  rankcf  9176  ltresr  9538  ltxrlt  9676  wloglei  10110  ltxr  11353  xrltnr  11359  xrltnsym  11372  xrlttri  11374  xrlttr  11375  brfi1uzind  12532  f1olecpbl  14924  isfull  15279  isfth  15283  prslem  15560  pslem  15836  dirtr  15866  xrsdsval  18462  dvcvx  22421  axcontlem9  24275  iscusgra  24456  sizeusglecusg  24486  iswlkon  24534  istrlon  24543  ispth  24570  isspth  24571  ispthon  24578  0pthonv  24583  isspthon  24585  1pthon2v  24595  2pthon3v  24606  usg2wlk  24617  usg2wlkon  24618  constr3cyclpe  24663  3v3e3cycl2  24664  isclwlk0  24754  isrusgra  24927  iseupa  24965  dfrel4  27454  2sqmo  27637  mclsppslem  28943  dfpo2  29184  fununiq  29200  elfix2  29554  monotoddzzfi  30878  wlkc  32350  lindepsnlininds  33053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator