Theorem breq1i 4660

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

Syntax hints:   ↔ wb 196   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  eqbrtri  4674  brtpos0  7359  brtpos  7361  euen1  8026  euen1b  8027  2dom  8029  0sdom1dom  8158  modom2  8162  1sdom  8163  infglb  8396  infglbb  8397  cnfcom3lem  8600  pr2nelem  8827  axdclem2  9342  rnct  9347  cfpwsdom  9406  inar1  9597  reclem3pr  9871  gt0srpr  9899  mappsrpr  9929  ltpsrpr  9930  map2psrpr  9931  axpre-mulgt0  9989  lt0neg1  10534  le0neg1  10536  reclt1  10918  addltmul  11268  eluz2b1  11759  xlt0neg1  12050  xle0neg1  12052  iccshftr  12306  iccshftl  12308  iccdil  12310  icccntr  12312  elfznelfzo  12573  bernneq  12990  nn0opthlem1  13055  faclbnd4lem1  13080  hashge0  13176  hashge2el2difr  13263  cbvsum  14425  divcnvshft  14587  cbvprod  14645  iprodmul  14734  oddge22np1  15073  nn0o1gt2  15097  divalglem1  15117  divalglem6  15121  isprm3  15396  dvdsnprmd  15403  prmgaplem3  15757  isnzr2  19263  chrdvds  19876  chrcong  19877  lindsmm  20167  cpmidpmat  20678  csdfil  21698  iscau3  23076  ioombl1lem4  23329  itg2cn  23530  radcnvlt1  24172  sincosq1sgn  24250  sincosq3sgn  24252  sincosq4sgn  24253  ang180lem3  24541  leibpilem2  24668  issqf  24862  bposlem6  25014  gausslemma2dlem3  25093  clwlkclwwlklem2  26901  konigsberglem5  27118  cvexchi  29228  addltmulALT  29305  dya2iocct  30342  ballotlemi1  30564  signswch  30638  cos2h  33400  tan2h  33401  lhpocnel2  35305  cdlemk19w  36260  rencldnfilem  37384  frege70  38227  frege118  38275  hashnzfzclim  38521  dvradcnv2  38546  binomcxplemnotnn0  38555  supxrleubrnmptf  39680  ioonct  39764  fourierdlem112  40435  salexct2  40557  flsqrt5  41509  lighneallem4b  41526  gbegt5  41649  gbowgt5  41650  gbowge7  41651  gbege6  41653  sbgoldbwt  41665  sbgoldbst  41666  sbgoldbalt  41669  sbgoldbm  41672  nnsum3primesle9  41682  nnsum4primesevenALTV  41689  bgoldbtbndlem1  41693  tgblthelfgott  41703  tgblthelfgottOLD  41709  difmodm1lt  42317