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

Theorem breq1i 4007
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 4003 . 2 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
31, 2ax-mp 5 1 (𝐴𝑅𝐶𝐵𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wb 105   = wceq 1353   class class class wbr 4000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600  df-br 4001
This theorem is referenced by:  eqbrtri  4021  brtpos0  6246  euen1  6795  euen1b  6796  2dom  6798  infglbti  7017  pr2nelem  7183  caucvgprprlemnbj  7670  caucvgprprlemmu  7672  caucvgprprlemaddq  7685  caucvgprprlem1  7686  gt0srpr  7725  caucvgsr  7779  mappsrprg  7781  map2psrprg  7782  pitonnlem1  7822  pitoregt0  7826  axprecex  7857  axpre-mulgt0  7864  axcaucvglemres  7876  lt0neg1  8402  le0neg1  8404  reclt1  8829  addltmul  9131  eluz2b1  9577  nn01to3  9593  xlt0neg1  9812  xle0neg1  9814  iccshftr  9968  iccshftl  9970  iccdil  9972  icccntr  9974  bernneq  10613  cbvsum  11339  expcnv  11483  cbvprod  11537  oddge22np1  11856  nn0o1gt2  11880  isprm3  12088  dvdsnprmd  12095  pw2dvdslemn  12135  txmetcnp  13651  sincosq1sgn  13880  sincosq3sgn  13882  sincosq4sgn  13883  logrpap0b  13930
  Copyright terms: Public domain W3C validator