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  27464  slt0neg2d  27528  mulscut  27591  lfgrwlkprop  28975  konigsberglem4  29539  frgrwopreglem2  29597  avril1  29747  minvecolem5  30165  minvecolem6  30166  minvecolem7  30167  bcsiALT  30463  pjdifnormii  30967  cvexchi  31653  ballotlem4  33528  bnj110  33900  wsuclb  34831  dalem18  38600  dalem48  38639  cdlemblem  38712  cdleme7ga  39167  cdlemg27b  39615  frege116  42778  frege120  42782  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  hoidmv1lelem3  45357  hoidmvlelem3  45361  hoidmvle  45364  257prm  46277  fmtno4prmfac  46288  fmtno4nprmfac193  46290  flsqrt5  46310  139prmALT  46312  31prm  46313  127prm  46315  lighneallem2  46322  stgoldbwt  46492  nnsum3primesle9  46510  wtgoldbnnsum4prm  46518  bgoldbnnsum3prm  46520  lincdifsn  47153  lindslinindsimp1  47186  lindslinindsimp2lem5  47191  lindslinindsimp2  47192  fldivexpfllog2  47299  nnlog2ge0lt1  47300  blen1b  47322  resum2sqorgt0  47443