Theorem breq2i 5157

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

Syntax hints:   ↔ wb 205   = wceq 1542   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  breqtri  5174  en1  9021  en1OLD  9022  snnen2oOLD  9227  sdom1  9242  enp1i  9279  enp1iOLD  9280  pm54.43  9996  addclprlem2  11012  map2psrpr  11105  lt0neg2  11721  le0neg2  11723  recgt1  12110  addltmul  12448  nn0lt2  12625  3halfnz  12641  xlt0neg2  13199  xle0neg2  13201  iccshftr  13463  iccshftl  13465  iccdil  13467  icccntr  13469  hashen1  14330  swrdccatin2  14679  pfxccat3  14684  mertens  15832  aleph1re  16188  dvdslelem  16252  3dvdsdec  16275  3dvds2dec  16276  divalglem5  16340  ndvdsi  16355  bitsfzo  16376  absproddvds  16554  prmfac1  16658  prm23lt5  16747  dec2dvds  16996  dec5dvds2  16998  prmlem0  17039  dprd0  19901  ablfac1lem  19938  minveclem3b  24945  minveclem6  24951  minveclem7  24952  ioombl1lem4  25078  sinhalfpilem  25973  sincosq1lem  26007  sincosq1sgn  26008  sincosq2sgn  26009  sincosq3sgn  26010  sincosq4sgn  26011  bposlem6  26792  gausslemma2dlem1a  26868  2lgsoddprmlem3  26917  nosupinfsep  27235  addscut  27462  slt0neg2d  27525  mulscut  27588  lfgrwlkprop  28944  konigsberglem4  29508  frgrwopreglem2  29566  avril1  29716  minvecolem5  30134  minvecolem6  30135  minvecolem7  30136  bcsiALT  30432  pjdifnormii  30936  cvexchi  31622  ballotlem4  33497  bnj110  33869  wsuclb  34800  dalem18  38552  dalem48  38591  cdlemblem  38664  cdleme7ga  39119  cdlemg27b  39567  frege116  42730  frege120  42734  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  hoidmv1lelem3  45309  hoidmvlelem3  45313  hoidmvle  45316  257prm  46229  fmtno4prmfac  46240  fmtno4nprmfac193  46242  flsqrt5  46262  139prmALT  46264  31prm  46265  127prm  46267  lighneallem2  46274  stgoldbwt  46444  nnsum3primesle9  46462  wtgoldbnnsum4prm  46470  bgoldbnnsum3prm  46472  lincdifsn  47105  lindslinindsimp1  47138  lindslinindsimp2lem5  47143  lindslinindsimp2  47144  fldivexpfllog2  47251  nnlog2ge0lt1  47252  blen1b  47274  resum2sqorgt0  47395