Theorem breq1i 4093

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

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

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  eqbrtri  4107  brtpos0  6413  euen1  6971  euen1b  6972  2dom  6975  modom2  6990  infglbti  7215  pr2nelem  7387  pr2cv2  7392  caucvgprprlemnbj  7903  caucvgprprlemmu  7905  caucvgprprlemaddq  7918  caucvgprprlem1  7919  gt0srpr  7958  caucvgsr  8012  mappsrprg  8014  map2psrprg  8015  pitonnlem1  8055  pitoregt0  8059  axprecex  8090  axpre-mulgt0  8097  axcaucvglemres  8109  lt0neg1  8638  le0neg1  8640  reclt1  9066  addltmul  9371  eluz2b1  9825  nn01to3  9841  xlt0neg1  10063  xle0neg1  10065  iccshftr  10219  iccshftl  10221  iccdil  10223  icccntr  10225  bernneq  10912  cbvsum  11911  expcnv  12055  cbvprod  12109  oddge22np1  12432  nn0o1gt2  12456  isprm3  12680  dvdsnprmd  12687  pw2dvdslemn  12727  txmetcnp  15232  sincosq1sgn  15540  sincosq3sgn  15542  sincosq4sgn  15543  logrpap0b  15590  gausslemma2dlem3  15782