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

Theorem breq2i 4445
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 4441 . 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 1383   class class class wbr 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438
This theorem is referenced by:  breqtri  4460  en1  7584  snnen2o  7708  enp1i  7757  pm54.43  8384  addclprlem2  9398  map2psrpr  9490  lt0neg2  10065  le0neg2  10067  recgt1  10447  addltmul  10780  nn0lt10bOLD  10932  nn0lt2  10933  xlt0neg2  11428  xle0neg2  11430  iccshftr  11663  iccshftl  11665  iccdil  11667  icccntr  11669  hashen1  12418  swrdccatin2  12691  swrdccat3  12696  mertens  13674  aleph1re  13855  dvdslelem  13907  divalglem5  13932  ndvdsi  13945  bitsfzo  13962  3prm  14111  prmfac1  14136  dec2dvds  14426  dec5dvds2  14428  prmlem0  14468  dprd0  16952  ablfac1lem  16993  minveclem3b  21716  minveclem6  21722  minveclem7  21723  ioombl1lem4  21844  sinhalfpilem  22728  sincosq1lem  22762  sincosq1sgn  22763  sincosq2sgn  22764  sincosq3sgn  22765  sincosq4sgn  22766  bposlem6  23436  avril1  25043  minvecolem5  25669  minvecolem6  25670  minvecolem7  25671  bcsiALT  25968  pjdifnormii  26473  cvexchi  27160  ballotlem4  28310  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  lincdifsn  32755  lindslinindsimp1  32788  lindslinindsimp2lem5  32793  lindslinindsimp2  32794  bnj110  33644  dalem18  35139  dalem48  35178  cdlemblem  35251  cdleme7ga  35707  cdlemg27b  36156  frege72  37626
  Copyright terms: Public domain W3C validator