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

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

Proof of Theorem breq2i
StepHypRef Expression
1 breq1i.1 . 2  |-  A  =  B
2 breq2 4291 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2ax-mp 5 1  |-  ( C R A  <->  C R B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1369   class class class wbr 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288
This theorem is referenced by:  breqtri  4310  en1  7368  enp1i  7539  pm54.43  8162  addclprlem2  9178  map2psrpr  9269  lt0neg2  9838  le0neg2  9840  recgt1  10220  addltmul  10552  nn0lt10b  10698  xlt0neg2  11182  xle0neg2  11184  iccshftr  11411  iccshftl  11413  iccdil  11415  icccntr  11417  swrdccatin2  12370  swrdccat3  12375  mertens  13338  aleph1re  13519  dvdslelem  13569  divalglem5  13593  ndvdsi  13606  bitsfzo  13623  3prm  13772  prmfac1  13796  dec2dvds  14084  dec5dvds2  14086  prmlem0  14125  dprd0  16516  ablfac1lem  16557  ply1coe  17721  minveclem3b  20890  minveclem6  20896  minveclem7  20897  ioombl1lem4  21017  sinhalfpilem  21900  sincosq1lem  21934  sincosq1sgn  21935  sincosq2sgn  21936  sincosq3sgn  21937  sincosq4sgn  21938  bposlem6  22603  avril1  23607  minvecolem5  24233  minvecolem6  24234  minvecolem7  24235  bcsiALT  24532  pjdifnormii  25037  cvexchi  25724  gsumle  26197  ballotlem4  26833  nn0lt2  30139  hashen1  30689  snnen2o  30690  lincdifsn  30847  lindslinindsimp1  30880  lindslinindsimp2lem5  30885  lindslinindsimp2  30886  bnj110  31738  dalem18  33165  dalem48  33204  cdlemblem  33277  cdleme7ga  33732  cdlemg27b  34180
  Copyright terms: Public domain W3C validator