Theorem breq2i 4883

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

Syntax hints:   ↔ wb 198   = wceq 1656   class class class wbr 4875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-br 4876

This theorem is referenced by:  breqtri  4900  en1  8295  snnen2o  8424  enp1i  8470  pm54.43  9146  addclprlem2  10161  map2psrpr  10254  lt0neg2  10866  le0neg2  10868  recgt1  11256  addltmul  11601  nn0lt2  11775  3halfnz  11791  xlt0neg2  12346  xle0neg2  12348  iccshftr  12606  iccshftl  12608  iccdil  12610  icccntr  12612  hashen1  13457  swrdccatin2  13833  pfxccat3  13840  swrdccat3OLD  13841  mertens  14998  aleph1re  15355  dvdslelem  15415  3dvdsdec  15437  3dvds2dec  15438  divalglem5  15501  ndvdsi  15516  bitsfzo  15537  absproddvds  15710  3prm  15785  prmfac1  15809  prm23lt5  15897  dec2dvds  16145  dec5dvds2  16147  prmlem0  16185  dprd0  18791  ablfac1lem  18828  minveclem3b  23603  minveclem6  23609  minveclem7  23610  ioombl1lem4  23734  sinhalfpilem  24622  sincosq1lem  24656  sincosq1sgn  24657  sincosq2sgn  24658  sincosq3sgn  24659  sincosq4sgn  24660  bposlem6  25434  gausslemma2dlem1a  25510  2lgsoddprmlem3  25559  lfgrwlkprop  26995  konigsberglem4  27630  frgrwopreglem2  27690  avril1  27873  minvecolem5  28288  minvecolem6  28289  minvecolem7  28290  bcsiALT  28587  pjdifnormii  29093  cvexchi  29779  ballotlem4  31102  bnj110  31470  wsuclb  32307  dalem18  35751  dalem48  35790  cdlemblem  35863  cdleme7ga  36318  cdlemg27b  36766  frege116  39108  frege120  39112  ioodvbdlimc1lem2  40936  ioodvbdlimc2lem  40938  hoidmv1lelem3  41595  hoidmvlelem3  41599  hoidmvle  41602  257prm  42317  fmtno4prmfac  42328  fmtno4nprmfac193  42330  flsqrt5  42353  139prmALT  42355  31prm  42356  127prm  42359  lighneallem2  42367  stgoldbwt  42508  nnsum3primesle9  42526  wtgoldbnnsum4prm  42534  bgoldbnnsum3prm  42536  lincdifsn  43074  lindslinindsimp1  43107  lindslinindsimp2lem5  43112  lindslinindsimp2  43113  fldivexpfllog2  43220  nnlog2ge0lt1  43221  blen1b  43243