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

Theorem breq1i 4067
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 4063 . 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 1633   class class class wbr 4060
This theorem is referenced by:  eqbrtri  4079  brtpos0  6283  brtpos  6285  euen1  6974  euen1b  6975  2dom  6976  0sdom1dom  7103  modom2  7107  1sdom  7108  cnfcom3lem  7451  pr2nelem  7679  axdclem2  8192  cfpwsdom  8251  inar1  8442  reclem3pr  8718  gt0srpr  8745  mappsrpr  8775  ltpsrpr  8776  map2psrpr  8777  axpre-mulgt0  8835  lt0neg1  9325  le0neg1  9327  reclt1  9696  addltmul  9994  recnz  10134  uzindOLD  10153  eluz2b1  10336  xlt0neg1  10593  xle0neg1  10595  iccshftr  10816  iccshftl  10818  iccdil  10820  icccntr  10822  bernneq  11274  nn0opthlem1  11330  faclbnd4lem1  11353  divalglem1  12640  divalglem6  12644  isprm2lem  12812  isprm3  12814  isnzr2  16064  chrdvds  16538  chrcong  16539  csdfil  17641  iscau3  18757  ioombl1lem4  18971  itg2cn  19171  radcnvlt1  19847  sincosq1sgn  19919  sincosq3sgn  19921  sincosq4sgn  19922  ang180lem3  20162  leibpilem2  20290  issqf  20427  bposlem6  20581  cvexchi  23004  addltmulALT  23081  dmct  23256  rnct  23258  abrexct  23261  abrexctf  23263  hashge0  23308  dya2icoseg  23801  dya2iocct  23804  ballotlem2  23920  ballotlemi1  23934  divcnvshft  24392  cbvprod  24418  iprodmul  24475  lindsmm  26446  fmul01lt1lem2  26863  elfznelfzo  27275  frgra3v  27594  3vfriswmgra  27597  lhpocnel2  30026  cdlemk19w  30979
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