Theorem breq1i 4089

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

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		breq1 4085	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)

Syntax hints:   ↔ wb 105   = wceq 1395   class class class wbr 4082

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083

This theorem is referenced by:  eqbrtri  4103  brtpos0  6396  euen1  6952  euen1b  6953  2dom  6956  infglbti  7188  pr2nelem  7360  pr2cv2  7365  caucvgprprlemnbj  7876  caucvgprprlemmu  7878  caucvgprprlemaddq  7891  caucvgprprlem1  7892  gt0srpr  7931  caucvgsr  7985  mappsrprg  7987  map2psrprg  7988  pitonnlem1  8028  pitoregt0  8032  axprecex  8063  axpre-mulgt0  8070  axcaucvglemres  8082  lt0neg1  8611  le0neg1  8613  reclt1  9039  addltmul  9344  eluz2b1  9792  nn01to3  9808  xlt0neg1  10030  xle0neg1  10032  iccshftr  10186  iccshftl  10188  iccdil  10190  icccntr  10192  bernneq  10877  cbvsum  11866  expcnv  12010  cbvprod  12064  oddge22np1  12387  nn0o1gt2  12411  isprm3  12635  dvdsnprmd  12642  pw2dvdslemn  12682  txmetcnp  15186  sincosq1sgn  15494  sincosq3sgn  15496  sincosq4sgn  15497  logrpap0b  15544  gausslemma2dlem3  15736