Theorem breq1i 4090

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

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

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 4084

This theorem is referenced by:  eqbrtri  4104  brtpos0  6404  euen1  6962  euen1b  6963  2dom  6966  infglbti  7203  pr2nelem  7375  pr2cv2  7380  caucvgprprlemnbj  7891  caucvgprprlemmu  7893  caucvgprprlemaddq  7906  caucvgprprlem1  7907  gt0srpr  7946  caucvgsr  8000  mappsrprg  8002  map2psrprg  8003  pitonnlem1  8043  pitoregt0  8047  axprecex  8078  axpre-mulgt0  8085  axcaucvglemres  8097  lt0neg1  8626  le0neg1  8628  reclt1  9054  addltmul  9359  eluz2b1  9808  nn01to3  9824  xlt0neg1  10046  xle0neg1  10048  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  bernneq  10894  cbvsum  11886  expcnv  12030  cbvprod  12084  oddge22np1  12407  nn0o1gt2  12431  isprm3  12655  dvdsnprmd  12662  pw2dvdslemn  12702  txmetcnp  15207  sincosq1sgn  15515  sincosq3sgn  15517  sincosq4sgn  15518  logrpap0b  15565  gausslemma2dlem3  15757