Theorem breq2i 5132

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

Syntax hints:   ↔ wb 206   = wceq 1540   class class class wbr 5124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  breqtri  5149  en1  9043  snnen2oOLD  9241  sdom1  9255  enp1i  9290  enp1iOLD  9291  pm54.43  10020  addclprlem2  11036  map2psrpr  11129  lt0neg2  11749  le0neg2  11751  recgt1  12143  addltmul  12482  nn0lt2  12661  3halfnz  12677  xlt0neg2  13241  xle0neg2  13243  iccshftr  13508  iccshftl  13510  iccdil  13512  icccntr  13514  hashen1  14393  swrdccatin2  14752  pfxccat3  14757  mertens  15907  aleph1re  16268  dvdslelem  16333  3dvdsdec  16356  3dvds2dec  16357  divalglem5  16421  ndvdsi  16436  bitsfzo  16459  absproddvds  16641  prmfac1  16744  prm23lt5  16839  dec2dvds  17088  dec5dvds2  17090  prmlem0  17130  dprd0  20019  ablfac1lem  20056  minveclem3b  25385  minveclem6  25391  minveclem7  25392  ioombl1lem4  25519  sinhalfpilem  26429  sincosq1lem  26463  sincosq1sgn  26464  sincosq2sgn  26465  sincosq3sgn  26466  sincosq4sgn  26467  bposlem6  27257  gausslemma2dlem1a  27333  2lgsoddprmlem3  27382  nosupinfsep  27701  addscut  27942  slt0neg2d  28014  mulscut  28092  abssneg  28206  elnnzs  28346  lfgrwlkprop  29672  konigsberglem4  30241  frgrwopreglem2  30299  avril1  30449  minvecolem5  30867  minvecolem6  30868  minvecolem7  30869  bcsiALT  31165  pjdifnormii  31669  cvexchi  32355  fldext2chn  33767  ballotlem4  34536  bnj110  34894  wsuclb  35851  dalem18  39705  dalem48  39744  cdlemblem  39817  cdleme7ga  40272  cdlemg27b  40720  frege116  43970  frege120  43974  ioodvbdlimc1lem2  45928  ioodvbdlimc2lem  45930  hoidmv1lelem3  46589  hoidmvlelem3  46593  hoidmvle  46596  257prm  47542  fmtno4prmfac  47553  fmtno4nprmfac193  47555  flsqrt5  47575  139prmALT  47577  31prm  47578  127prm  47580  lighneallem2  47587  stgoldbwt  47757  nnsum3primesle9  47775  wtgoldbnnsum4prm  47783  bgoldbnnsum3prm  47785  lincdifsn  48367  lindslinindsimp1  48400  lindslinindsimp2lem5  48405  lindslinindsimp2  48406  fldivexpfllog2  48512  nnlog2ge0lt1  48513  blen1b  48535  resum2sqorgt0  48656