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

Theorem breq12i 4410
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 4406 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3mp2an 672 1  |-  ( A R C  <->  B R D )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1370   class class class wbr 4401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-br 4402
This theorem is referenced by:  3brtr3g  4432  3brtr4g  4433  caovord2  6386  domunfican  7696  ltsonq  9250  ltanq  9252  ltmnq  9253  prlem934  9314  prlem936  9328  ltsosr  9373  ltasr  9379  ltneg  9951  leneg  9954  inelr  10424  lt2sqi  12072  le2sqi  12073  nn0le2msqi  12163  axlowdimlem6  23346  mdsldmd1i  25888  divcnvlin  27544
  Copyright terms: Public domain W3C validator