Theorem breq2i 5150

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

Syntax hints:   ↔ wb 206   = wceq 1539   class class class wbr 5142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143

This theorem is referenced by:  breqtri  5167  en1  9065  snnen2oOLD  9265  sdom1  9279  enp1i  9314  enp1iOLD  9315  pm54.43  10042  addclprlem2  11058  map2psrpr  11151  lt0neg2  11771  le0neg2  11773  recgt1  12165  addltmul  12504  nn0lt2  12683  3halfnz  12699  xlt0neg2  13263  xle0neg2  13265  iccshftr  13527  iccshftl  13529  iccdil  13531  icccntr  13533  hashen1  14410  swrdccatin2  14768  pfxccat3  14773  mertens  15923  aleph1re  16282  dvdslelem  16347  3dvdsdec  16370  3dvds2dec  16371  divalglem5  16435  ndvdsi  16450  bitsfzo  16473  absproddvds  16655  prmfac1  16758  prm23lt5  16853  dec2dvds  17102  dec5dvds2  17104  prmlem0  17144  dprd0  20052  ablfac1lem  20089  minveclem3b  25463  minveclem6  25469  minveclem7  25470  ioombl1lem4  25597  sinhalfpilem  26506  sincosq1lem  26540  sincosq1sgn  26541  sincosq2sgn  26542  sincosq3sgn  26543  sincosq4sgn  26544  bposlem6  27334  gausslemma2dlem1a  27410  2lgsoddprmlem3  27459  nosupinfsep  27778  addscut  28012  slt0neg2d  28084  mulscut  28159  abssneg  28272  elnnzs  28388  lfgrwlkprop  29706  konigsberglem4  30275  frgrwopreglem2  30333  avril1  30483  minvecolem5  30901  minvecolem6  30902  minvecolem7  30903  bcsiALT  31199  pjdifnormii  31703  cvexchi  32389  fldext2chn  33770  ballotlem4  34502  bnj110  34873  wsuclb  35830  dalem18  39684  dalem48  39723  cdlemblem  39796  cdleme7ga  40251  cdlemg27b  40699  frege116  43997  frege120  44001  ioodvbdlimc1lem2  45952  ioodvbdlimc2lem  45954  hoidmv1lelem3  46613  hoidmvlelem3  46617  hoidmvle  46620  257prm  47553  fmtno4prmfac  47564  fmtno4nprmfac193  47566  flsqrt5  47586  139prmALT  47588  31prm  47589  127prm  47591  lighneallem2  47598  stgoldbwt  47768  nnsum3primesle9  47786  wtgoldbnnsum4prm  47794  bgoldbnnsum3prm  47796  lincdifsn  48346  lindslinindsimp1  48379  lindslinindsimp2lem5  48384  lindslinindsimp2  48385  fldivexpfllog2  48491  nnlog2ge0lt1  48492  blen1b  48514  resum2sqorgt0  48635