ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  breq1i GIF version

Theorem breq1i 3906
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
breq1i (𝐴𝑅𝐶𝐵𝑅𝐶)

Proof of Theorem breq1i
StepHypRef Expression
1 breq1i.1 . 2 𝐴 = 𝐵
2 breq1 3902 . 2 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
31, 2ax-mp 5 1 (𝐴𝑅𝐶𝐵𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1316   class class class wbr 3899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900
This theorem is referenced by:  eqbrtri  3919  brtpos0  6117  euen1  6664  euen1b  6665  2dom  6667  infglbti  6880  pr2nelem  7015  caucvgprprlemnbj  7469  caucvgprprlemmu  7471  caucvgprprlemaddq  7484  caucvgprprlem1  7485  gt0srpr  7524  caucvgsr  7578  mappsrprg  7580  map2psrprg  7581  pitonnlem1  7621  pitoregt0  7625  axprecex  7656  axpre-mulgt0  7663  axcaucvglemres  7675  lt0neg1  8198  le0neg1  8200  reclt1  8622  addltmul  8924  eluz2b1  9363  nn01to3  9377  xlt0neg1  9589  xle0neg1  9591  iccshftr  9745  iccshftl  9747  iccdil  9749  icccntr  9751  bernneq  10380  cbvsum  11097  expcnv  11241  oddge22np1  11505  nn0o1gt2  11529  isprm3  11726  dvdsnprmd  11733  pw2dvdslemn  11770  txmetcnp  12614  sincosq1sgn  12834  sincosq3sgn  12836  sincosq4sgn  12837
  Copyright terms: Public domain W3C validator