Theorem breq1i 5075

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

Syntax hints:   ↔ wb 208   = wceq 1537   class class class wbr 5068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069

This theorem is referenced by:  eqbrtri  5089  brtpos0  7901  brtpos  7903  euen1  8581  euen1b  8582  2dom  8584  0sdom1dom  8718  modom2  8722  1sdom  8723  infglb  8956  infglbb  8957  cnfcom3lem  9168  pr2nelem  9432  axdclem2  9944  rnct  9949  cfpwsdom  10008  inar1  10199  reclem3pr  10473  gt0srpr  10502  mappsrpr  10532  ltpsrpr  10533  map2psrpr  10534  axpre-mulgt0  10592  lt0neg1  11148  le0neg1  11150  reclt1  11537  addltmul  11876  eluz2b1  12322  xlt0neg1  12615  xle0neg1  12617  iccshftr  12875  iccshftl  12877  iccdil  12879  icccntr  12881  elfznelfzo  13145  bernneq  13593  nn0opthlem1  13631  faclbnd4lem1  13656  hashge0  13751  hashgt23el  13788  hashge2el2difr  13842  cbvsum  15054  divcnvshft  15212  cbvprod  15271  iprodmul  15359  oddge22np1  15700  nn0o1gt2  15734  divalglem1  15747  divalglem6  15751  isprm3  16029  dvdsnprmd  16036  2mulprm  16039  ge2nprmge4  16047  prmgaplem3  16391  isnzr2  20038  chrdvds  20677  chrcong  20678  lindsmm  20974  cpmidpmat  21483  csdfil  22504  iscau3  23883  ioombl1lem4  24164  itg2cn  24366  radcnvlt1  25008  sincosq1sgn  25086  sincosq3sgn  25088  sincosq4sgn  25089  ang180lem3  25391  leibpilem2  25521  issqf  25715  bposlem6  25867  gausslemma2dlem3  25946  clwlkclwwlklem2  27780  clwlkclwwlk2  27783  clwlkclwwlkf  27788  clwlknf1oclwwlknlem1  27862  konigsberglem5  28037  cvexchi  30148  addltmulALT  30225  xnn01gt  30497  dya2iocct  31540  ballotlemi1  31762  signswch  31833  usgrgt2cycl  32379  cusgracyclt3v  32405  cos2h  34885  tan2h  34886  lhpocnel2  37157  cdlemk19w  38110  rencldnfilem  39424  frege70  40286  frege118  40334  hashnzfzclim  40661  dvradcnv2  40686  binomcxplemnotnn0  40695  supxrleubrnmptf  41734  ioonct  41820  fourierdlem112  42510  salexct2  42629  flsqrt5  43764  lighneallem4b  43781  fpprel2  43913  gbegt5  43933  gbowgt5  43934  gbowge7  43935  gbege6  43937  sbgoldbwt  43949  sbgoldbst  43950  sbgoldbalt  43953  sbgoldbm  43956  nnsum3primesle9  43966  nnsum4primesevenALTV  43973  bgoldbtbndlem1  43977  tgblthelfgott  43987  difmodm1lt  44589