Theorem breq2i 4661

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

Syntax hints:   ↔ wb 196   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  breqtri  4678  en1  8023  snnen2o  8149  enp1i  8195  pm54.43  8826  addclprlem2  9839  map2psrpr  9931  lt0neg2  10535  le0neg2  10537  recgt1  10919  addltmul  11268  nn0lt2  11440  3halfnz  11456  declecOLD  11544  xlt0neg2  12051  xle0neg2  12053  iccshftr  12306  iccshftl  12308  iccdil  12310  icccntr  12312  hashen1  13160  swrdccatin2  13487  swrdccat3  13492  mertens  14618  aleph1re  14974  dvdslelem  15031  3dvdsdec  15054  3dvdsdecOLD  15055  3dvds2dec  15056  3dvds2decOLD  15057  divalglem5  15120  ndvdsi  15136  bitsfzo  15157  absproddvds  15330  3prm  15406  prmfac1  15431  prm23lt5  15519  dec2dvds  15767  dec5dvds2  15769  prmlem0  15812  dprd0  18430  ablfac1lem  18467  minveclem3b  23199  minveclem6  23205  minveclem7  23206  ioombl1lem4  23329  sinhalfpilem  24215  sincosq1lem  24249  sincosq1sgn  24250  sincosq2sgn  24251  sincosq3sgn  24252  sincosq4sgn  24253  bposlem6  25014  gausslemma2dlem1a  25090  2lgsoddprmlem3  25139  lfgrwlkprop  26584  konigsberglem4  27117  frgrwopreglem2  27177  avril1  27319  minvecolem5  27737  minvecolem6  27738  minvecolem7  27739  bcsiALT  28036  pjdifnormii  28542  cvexchi  29228  ballotlem4  30560  bnj110  30928  wsuclb  31777  dalem18  34967  dalem48  35006  cdlemblem  35079  cdleme7ga  35535  cdlemg27b  35984  frege116  38273  frege120  38277  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  hoidmv1lelem3  40807  hoidmvlelem3  40811  hoidmvle  40814  pfxccat3  41426  257prm  41473  fmtno4prmfac  41484  fmtno4nprmfac193  41486  flsqrt5  41509  139prmALT  41511  31prm  41512  127prm  41515  lighneallem2  41523  stgoldbwt  41664  nnsum3primesle9  41682  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  lincdifsn  42213  lindslinindsimp1  42246  lindslinindsimp2lem5  42251  lindslinindsimp2  42252  fldivexpfllog2  42359  nnlog2ge0lt1  42360  blen1b  42382