Theorem breq1i 5073

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

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

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  eqbrtri  5087  brtpos0  7899  brtpos  7901  euen1  8579  euen1b  8580  2dom  8582  0sdom1dom  8716  modom2  8720  1sdom  8721  infglb  8954  infglbb  8955  cnfcom3lem  9166  pr2nelem  9430  axdclem2  9942  rnct  9947  cfpwsdom  10006  inar1  10197  reclem3pr  10471  gt0srpr  10500  mappsrpr  10530  ltpsrpr  10531  map2psrpr  10532  axpre-mulgt0  10590  lt0neg1  11146  le0neg1  11148  reclt1  11535  addltmul  11874  eluz2b1  12320  xlt0neg1  12613  xle0neg1  12615  iccshftr  12873  iccshftl  12875  iccdil  12877  icccntr  12879  elfznelfzo  13143  bernneq  13591  nn0opthlem1  13629  faclbnd4lem1  13654  hashge0  13749  hashgt23el  13786  hashge2el2difr  13840  cbvsum  15052  divcnvshft  15210  cbvprod  15269  iprodmul  15357  oddge22np1  15698  nn0o1gt2  15732  divalglem1  15745  divalglem6  15749  isprm3  16027  dvdsnprmd  16034  2mulprm  16037  ge2nprmge4  16045  prmgaplem3  16389  isnzr2  20036  chrdvds  20675  chrcong  20676  lindsmm  20972  cpmidpmat  21481  csdfil  22502  iscau3  23881  ioombl1lem4  24162  itg2cn  24364  radcnvlt1  25006  sincosq1sgn  25084  sincosq3sgn  25086  sincosq4sgn  25087  ang180lem3  25389  leibpilem2  25519  issqf  25713  bposlem6  25865  gausslemma2dlem3  25944  clwlkclwwlklem2  27778  clwlkclwwlk2  27781  clwlkclwwlkf  27786  clwlknf1oclwwlknlem1  27860  konigsberglem5  28035  cvexchi  30146  addltmulALT  30223  xnn01gt  30495  dya2iocct  31538  ballotlemi1  31760  signswch  31831  usgrgt2cycl  32377  cusgracyclt3v  32403  cos2h  34898  tan2h  34899  lhpocnel2  37170  cdlemk19w  38123  rencldnfilem  39437  frege70  40299  frege118  40347  hashnzfzclim  40674  dvradcnv2  40699  binomcxplemnotnn0  40708  supxrleubrnmptf  41747  ioonct  41833  fourierdlem112  42523  salexct2  42642  flsqrt5  43777  lighneallem4b  43794  fpprel2  43926  gbegt5  43946  gbowgt5  43947  gbowge7  43948  gbege6  43950  sbgoldbwt  43962  sbgoldbst  43963  sbgoldbalt  43966  sbgoldbm  43969  nnsum3primesle9  43979  nnsum4primesevenALTV  43986  bgoldbtbndlem1  43990  tgblthelfgott  44000  difmodm1lt  44602