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

Theorem breq12i 4069
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
Hypotheses
Ref Expression
breq1i.1  |-  A  =  B
breq12i.2  |-  C  =  D
Assertion
Ref Expression
breq12i  |-  ( A R C  <->  B R D )

Proof of Theorem breq12i
StepHypRef Expression
1 breq1i.1 . 2  |-  A  =  B
2 breq12i.2 . 2  |-  C  =  D
3 breq12 4065 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3mp2an 653 1  |-  ( A R C  <->  B R D )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1633   class class class wbr 4060
This theorem is referenced by:  3brtr3g  4091  3brtr4g  4092  caovord2  6074  domunfican  7174  ltsonq  8638  ltanq  8640  ltmnq  8641  prlem934  8702  prlem936  8716  ltsosr  8761  ltasr  8767  ltneg  9319  leneg  9322  inelr  9781  lt2sqi  11239  le2sqi  11240  nn0le2msqi  11329  mdsldmd1i  22966  divcnvlin  24393  axlowdimlem6  24961
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-br 4061
  Copyright terms: Public domain W3C validator