Theorem breq2i 5105

Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
breq2i	⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)

Proof of Theorem breq2i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		breq2 5101	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)

Syntax hints:   ↔ wb 206   = wceq 1542   class class class wbr 5097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  breqtri  5122  en1  8963  sdom1  9152  enp1i  9181  pm54.43  9915  addclprlem2  10930  map2psrpr  11023  lt0neg2  11646  le0neg2  11648  recgt1  12040  inelr  12137  addltmul  12379  nn0lt2  12557  3halfnz  12573  xlt0neg2  13137  xle0neg2  13139  iccshftr  13404  iccshftl  13406  iccdil  13408  icccntr  13410  hashen1  14295  swrdccatin2  14654  pfxccat3  14659  mertens  15811  aleph1re  16172  dvdslelem  16238  3dvdsdec  16261  3dvds2dec  16262  divalglem5  16326  ndvdsi  16341  bitsfzo  16364  absproddvds  16546  prmfac1  16649  prm23lt5  16744  dec2dvds  16993  dec5dvds2  16995  prmlem0  17035  dprd0  19964  ablfac1lem  20001  minveclem3b  25386  minveclem6  25392  minveclem7  25393  ioombl1lem4  25520  sinhalfpilem  26430  sincosq1lem  26464  sincosq1sgn  26465  sincosq2sgn  26466  sincosq3sgn  26467  sincosq4sgn  26468  bposlem6  27258  gausslemma2dlem1a  27334  2lgsoddprmlem3  27383  nosupinfsep  27702  addscut  27958  slt0neg2d  28031  mulscut  28112  abssneg  28226  n0slt1e0  28345  elnnzs  28378  avgslt1d  28430  avgslt2d  28431  bdaypw2n0sbndlem  28440  zs12bdaylem1  28447  lfgrwlkprop  29740  konigsberglem4  30311  frgrwopreglem2  30369  avril1  30519  minvecolem5  30937  minvecolem6  30938  minvecolem7  30939  bcsiALT  31235  pjdifnormii  31739  cvexchi  32425  fldext2chn  33864  ballotlem4  34635  bnj110  34993  wsuclb  35999  dalem18  39976  dalem48  40015  cdlemblem  40088  cdleme7ga  40543  cdlemg27b  40991  sn-inelr  42779  frege116  44257  frege120  44261  ioodvbdlimc1lem2  46213  ioodvbdlimc2lem  46215  hoidmv1lelem3  46874  hoidmvlelem3  46878  hoidmvle  46881  257prm  47844  fmtno4prmfac  47855  fmtno4nprmfac193  47857  flsqrt5  47877  139prmALT  47879  31prm  47880  127prm  47882  lighneallem2  47889  stgoldbwt  48059  nnsum3primesle9  48077  wtgoldbnnsum4prm  48085  bgoldbnnsum3prm  48087  lincdifsn  48707  lindslinindsimp1  48740  lindslinindsimp2lem5  48745  lindslinindsimp2  48746  fldivexpfllog2  48848  nnlog2ge0lt1  48849  blen1b  48871  resum2sqorgt0  48992