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

Theorem breq1i 4030
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1i.1  |-  A  =  B
Assertion
Ref Expression
breq1i  |-  ( A R C  <->  B R C )

Proof of Theorem breq1i
StepHypRef Expression
1 breq1i.1 . 2  |-  A  =  B
2 breq1 4026 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
31, 2ax-mp 8 1  |-  ( A R C  <->  B R C )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  eqbrtri  4042  brtpos0  6241  brtpos  6243  euen1  6931  euen1b  6932  2dom  6933  0sdom1dom  7060  modom2  7064  1sdom  7065  cnfcom3lem  7406  pr2nelem  7634  axdclem2  8147  cfpwsdom  8206  inar1  8397  reclem3pr  8673  gt0srpr  8700  mappsrpr  8730  ltpsrpr  8731  map2psrpr  8732  axpre-mulgt0  8790  lt0neg1  9280  le0neg1  9282  reclt1  9651  addltmul  9947  recnz  10087  uzindOLD  10106  eluz2b1  10289  xlt0neg1  10546  xle0neg1  10548  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  bernneq  11227  nn0opthlem1  11283  faclbnd4lem1  11306  divalglem1  12593  divalglem6  12597  isprm2lem  12765  isprm3  12767  isnzr2  16015  chrdvds  16482  chrcong  16483  csdfil  17589  iscau3  18704  ioombl1lem4  18918  itg2cn  19118  radcnvlt1  19794  sincosq1sgn  19866  sincosq3sgn  19868  sincosq4sgn  19869  ang180lem3  20109  leibpilem2  20237  issqf  20374  bposlem6  20528  cvexchi  22949  addltmulALT  23026  ballotlem2  23047  ballotlemi1  23061  dmct  23342  rnct  23344  abrexct  23347  abrexctf  23349  hashge0  23386  dya2iocseg  23579  dya2iocct  23581  lindsmm  27298  fmul01lt1lem2  27715  frgra3v  28180  3vfriswmgra  28183  lhpocnel2  30208  cdlemk19w  31161
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator