Theorem breq1i 4036

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

Syntax hints:   ↔ wb 105   = wceq 1364   class class class wbr 4029

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030

This theorem is referenced by:  eqbrtri  4050  brtpos0  6305  euen1  6856  euen1b  6857  2dom  6859  infglbti  7084  pr2nelem  7251  caucvgprprlemnbj  7753  caucvgprprlemmu  7755  caucvgprprlemaddq  7768  caucvgprprlem1  7769  gt0srpr  7808  caucvgsr  7862  mappsrprg  7864  map2psrprg  7865  pitonnlem1  7905  pitoregt0  7909  axprecex  7940  axpre-mulgt0  7947  axcaucvglemres  7959  lt0neg1  8487  le0neg1  8489  reclt1  8915  addltmul  9219  eluz2b1  9666  nn01to3  9682  xlt0neg1  9904  xle0neg1  9906  iccshftr  10060  iccshftl  10062  iccdil  10064  icccntr  10066  bernneq  10731  cbvsum  11503  expcnv  11647  cbvprod  11701  oddge22np1  12022  nn0o1gt2  12046  isprm3  12256  dvdsnprmd  12263  pw2dvdslemn  12303  txmetcnp  14686  sincosq1sgn  14961  sincosq3sgn  14963  sincosq4sgn  14964  logrpap0b  15011  gausslemma2dlem3  15179