Theorem breq1i 4050

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 4046	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)

Syntax hints:   ↔ wb 105   = wceq 1372   class class class wbr 4043

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044

This theorem is referenced by:  eqbrtri  4064  brtpos0  6337  euen1  6893  euen1b  6894  2dom  6896  infglbti  7126  pr2nelem  7298  caucvgprprlemnbj  7805  caucvgprprlemmu  7807  caucvgprprlemaddq  7820  caucvgprprlem1  7821  gt0srpr  7860  caucvgsr  7914  mappsrprg  7916  map2psrprg  7917  pitonnlem1  7957  pitoregt0  7961  axprecex  7992  axpre-mulgt0  7999  axcaucvglemres  8011  lt0neg1  8540  le0neg1  8542  reclt1  8968  addltmul  9273  eluz2b1  9721  nn01to3  9737  xlt0neg1  9959  xle0neg1  9961  iccshftr  10115  iccshftl  10117  iccdil  10119  icccntr  10121  bernneq  10803  cbvsum  11642  expcnv  11786  cbvprod  11840  oddge22np1  12163  nn0o1gt2  12187  isprm3  12411  dvdsnprmd  12418  pw2dvdslemn  12458  txmetcnp  14961  sincosq1sgn  15269  sincosq3sgn  15271  sincosq4sgn  15272  logrpap0b  15319  gausslemma2dlem3  15511