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

Theorem breq1i 4219
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 4215 . 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 177    = wceq 1652   class class class wbr 4212
This theorem is referenced by:  eqbrtri  4231  brtpos0  6486  brtpos  6488  euen1  7177  euen1b  7178  2dom  7179  0sdom1dom  7306  modom2  7310  1sdom  7311  cnfcom3lem  7660  pr2nelem  7888  axdclem2  8400  cfpwsdom  8459  inar1  8650  reclem3pr  8926  gt0srpr  8953  mappsrpr  8983  ltpsrpr  8984  map2psrpr  8985  axpre-mulgt0  9043  lt0neg1  9534  le0neg1  9536  reclt1  9905  addltmul  10203  recnz  10345  uzindOLD  10364  eluz2b1  10547  xlt0neg1  10805  xle0neg1  10807  iccshftr  11030  iccshftl  11032  iccdil  11034  icccntr  11036  elfznelfzo  11192  bernneq  11505  nn0opthlem1  11561  faclbnd4lem1  11584  hashge0  11661  hashle00  11669  divalglem1  12914  divalglem6  12918  isprm2lem  13086  isprm3  13088  isnzr2  16334  chrdvds  16809  chrcong  16810  csdfil  17926  iscau3  19231  ioombl1lem4  19455  itg2cn  19655  radcnvlt1  20334  sincosq1sgn  20406  sincosq3sgn  20408  sincosq4sgn  20409  ang180lem3  20653  leibpilem2  20781  issqf  20919  bposlem6  21073  cvexchi  23872  addltmulALT  23949  rnct  24108  dya2iocct  24630  ballotlemi1  24760  divcnvshft  25211  cbvprod  25241  iprodmul  25316  wsuclb  25579  lindsmm  27275  frgra3v  28392  3vfriswmgra  28395  lhpocnel2  30816  cdlemk19w  31769
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator