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

Theorem breq123d 4466
 Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
Hypotheses
Ref Expression
breq1d.1
breq123d.2
breq123d.3
Assertion
Ref Expression
breq123d

Proof of Theorem breq123d
StepHypRef Expression
1 breq1d.1 . . 3
2 breq123d.3 . . 3
31, 2breq12d 4465 . 2
4 breq123d.2 . . 3
54breqd 4463 . 2
63, 5bitrd 253 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  =wceq 1395   class class class wbr 4452 This theorem is referenced by:  sbcbr123  4503  sbcbrgOLD  4504  fmptco  6064  xpsle  14978  invfuc  15343  yonedainv  15550  opphllem3  24121  lmif  24151  islmib  24153  fmptcof2  27502  submomnd  27700  sgnsv  27717  inftmrel  27724  isinftm  27725  submarchi  27730  suborng  27805  fnwe2val  30995  aomclem8  31007  iscvlat  35048  paddfval  35521  lhpset  35719  tendofset  36484  diaffval  36757 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