Theorem breq2i 5108

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  breqtri  5125  en1  8975  sdom1  9164  enp1i  9193  pm54.43  9927  addclprlem2  10942  map2psrpr  11035  lt0neg2  11658  le0neg2  11660  recgt1  12052  inelr  12149  addltmul  12391  nn0lt2  12569  3halfnz  12585  xlt0neg2  13149  xle0neg2  13151  iccshftr  13416  iccshftl  13418  iccdil  13420  icccntr  13422  hashen1  14307  swrdccatin2  14666  pfxccat3  14671  mertens  15823  aleph1re  16184  dvdslelem  16250  3dvdsdec  16273  3dvds2dec  16274  divalglem5  16338  ndvdsi  16353  bitsfzo  16376  absproddvds  16558  prmfac1  16661  prm23lt5  16756  dec2dvds  17005  dec5dvds2  17007  prmlem0  17047  dprd0  19979  ablfac1lem  20016  minveclem3b  25401  minveclem6  25407  minveclem7  25408  ioombl1lem4  25535  sinhalfpilem  26445  sincosq1lem  26479  sincosq1sgn  26480  sincosq2sgn  26481  sincosq3sgn  26482  sincosq4sgn  26483  bposlem6  27273  gausslemma2dlem1a  27349  2lgsoddprmlem3  27398  nosupinfsep  27717  addcuts  27991  lt0negs2d  28064  mulcut  28145  absnegs  28260  n0lts1e0  28381  elnnzs  28414  avglts1d  28466  avglts2d  28467  bdaypw2n0bndlem  28476  z12bdaylem1  28483  lfgrwlkprop  29777  konigsberglem4  30348  frgrwopreglem2  30406  avril1  30556  minvecolem5  30975  minvecolem6  30976  minvecolem7  30977  bcsiALT  31273  pjdifnormii  31777  cvexchi  32463  fldext2chn  33912  ballotlem4  34683  bnj110  35040  wsuclb  36048  dalem18  40086  dalem48  40125  cdlemblem  40198  cdleme7ga  40653  cdlemg27b  41101  sn-inelr  42886  frege116  44364  frege120  44368  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  hoidmv1lelem3  46980  hoidmvlelem3  46984  hoidmvle  46987  257prm  47950  fmtno4prmfac  47961  fmtno4nprmfac193  47963  flsqrt5  47983  139prmALT  47985  31prm  47986  127prm  47988  lighneallem2  47995  stgoldbwt  48165  nnsum3primesle9  48183  wtgoldbnnsum4prm  48191  bgoldbnnsum3prm  48193  lincdifsn  48813  lindslinindsimp1  48846  lindslinindsimp2lem5  48851  lindslinindsimp2  48852  fldivexpfllog2  48954  nnlog2ge0lt1  48955  blen1b  48977  resum2sqorgt0  49098