Theorem breq2i 5114

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  breqtri  5133  en1  9076  sdom1  9266  enp1i  9295  pm54.43  10106  addclprlem2  11126  map2psrpr  11219  lt0neg2  11847  le0neg2  11849  recgt1  12237  inelr  12334  addltmul  12606  nn0lt2  12786  3halfnz  12802  xlt0neg2  13374  xle0neg2  13376  iccshftr  13641  iccshftl  13643  iccdil  13645  icccntr  13647  hashen1  14538  swrdccatin2  14903  pfxccat3  14908  mertens  16081  aleph1re  16439  dvdslelem  16505  3dvdsdec  16528  3dvds2dec  16529  divalglem5  16593  ndvdsi  16608  bitsfzo  16631  absproddvds  16818  prmfac1  16922  prm23lt5  17018  dec2dvds  17267  dec5dvds2  17269  prmlem0  17309  dprd0  20274  ablfac1lem  20311  minveclem3b  25776  minveclem6  25782  minveclem7  25783  ioombl1lem4  25909  sinhalfpilem  26819  sincosq1lem  26853  sincosq1sgn  26854  sincosq2sgn  26855  sincosq3sgn  26856  sincosq4sgn  26857  bposlem6  27643  gausslemma2dlem1a  27719  2lgsoddprmlem3  27768  nosupinfsep  28116  addcuts  28391  lt0negs2d  28464  mulcut  28545  absnegs  28660  n0lts1e0  28781  elnnzs  28814  avglts1d  28866  avglts2d  28867  bdaypw2n0bndlem  28876  z12bdaylem1  28883  lfgrwlkprop  30297  konigsberglem4  30883  frgrwopreglem2  30941  avril1  31091  minvecolem5  31510  minvecolem6  31511  minvecolem7  31512  bcsiALT  31808  pjdifnormii  32312  cvexchi  32998  fldext2chn  34427  ballotlem4  35198  bnj110  35555  wsuclb  36767  dalem18  40929  dalem48  40968  cdlemblem  41041  cdleme7ga  41496  cdlemg27b  41944  sn-inelr  43742  frege116  45169  frege120  45173  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  hoidmv1lelem3  47806  hoidmvlelem3  47810  hoidmvle  47813  257prm  48849  fmtno4prmfac  48860  fmtno4nprmfac193  48862  flsqrt5  48882  139prmALT  48884  31prm  48885  127prm  48887  lighneallem2  48894  nprmdvdsfacm1lem2  48909  stgoldbwt  49077  nnsum3primesle9  49095  wtgoldbnnsum4prm  49103  bgoldbnnsum3prm  49105  lincdifsn  49739  lindslinindsimp1  49772  lindslinindsimp2lem5  49777  lindslinindsimp2  49778  fldivexpfllog2  49880  nnlog2ge0lt1  49881  blen1b  49903  resum2sqorgt0  50024