Theorem breq2i 5097

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

Syntax hints:   ↔ wb 206   = wceq 1541   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  breqtri  5114  en1  8946  sdom1  9134  enp1i  9163  pm54.43  9894  addclprlem2  10908  map2psrpr  11001  lt0neg2  11624  le0neg2  11626  recgt1  12018  inelr  12115  addltmul  12357  nn0lt2  12536  3halfnz  12552  xlt0neg2  13119  xle0neg2  13121  iccshftr  13386  iccshftl  13388  iccdil  13390  icccntr  13392  hashen1  14277  swrdccatin2  14636  pfxccat3  14641  mertens  15793  aleph1re  16154  dvdslelem  16220  3dvdsdec  16243  3dvds2dec  16244  divalglem5  16308  ndvdsi  16323  bitsfzo  16346  absproddvds  16528  prmfac1  16631  prm23lt5  16726  dec2dvds  16975  dec5dvds2  16977  prmlem0  17017  dprd0  19945  ablfac1lem  19982  minveclem3b  25355  minveclem6  25361  minveclem7  25362  ioombl1lem4  25489  sinhalfpilem  26399  sincosq1lem  26433  sincosq1sgn  26434  sincosq2sgn  26435  sincosq3sgn  26436  sincosq4sgn  26437  bposlem6  27227  gausslemma2dlem1a  27303  2lgsoddprmlem3  27352  nosupinfsep  27671  addscut  27921  slt0neg2d  27993  mulscut  28071  abssneg  28185  elnnzs  28325  avgslt1d  28376  avgslt2d  28377  lfgrwlkprop  29664  konigsberglem4  30235  frgrwopreglem2  30293  avril1  30443  minvecolem5  30861  minvecolem6  30862  minvecolem7  30863  bcsiALT  31159  pjdifnormii  31663  cvexchi  32349  fldext2chn  33741  ballotlem4  34512  bnj110  34870  wsuclb  35870  dalem18  39779  dalem48  39818  cdlemblem  39891  cdleme7ga  40346  cdlemg27b  40794  sn-inelr  42579  frege116  44071  frege120  44075  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  hoidmv1lelem3  46690  hoidmvlelem3  46694  hoidmvle  46697  257prm  47660  fmtno4prmfac  47671  fmtno4nprmfac193  47673  flsqrt5  47693  139prmALT  47695  31prm  47696  127prm  47698  lighneallem2  47705  stgoldbwt  47875  nnsum3primesle9  47893  wtgoldbnnsum4prm  47901  bgoldbnnsum3prm  47903  lincdifsn  48524  lindslinindsimp1  48557  lindslinindsimp2lem5  48562  lindslinindsimp2  48563  fldivexpfllog2  48665  nnlog2ge0lt1  48666  blen1b  48688  resum2sqorgt0  48809