Theorem breq2i 5174

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

Syntax hints:   ↔ wb 206   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  breqtri  5191  en1  9086  en1OLD  9087  snnen2oOLD  9290  sdom1  9305  enp1i  9341  enp1iOLD  9342  pm54.43  10070  addclprlem2  11086  map2psrpr  11179  lt0neg2  11797  le0neg2  11799  recgt1  12191  addltmul  12529  nn0lt2  12706  3halfnz  12722  xlt0neg2  13282  xle0neg2  13284  iccshftr  13546  iccshftl  13548  iccdil  13550  icccntr  13552  hashen1  14419  swrdccatin2  14777  pfxccat3  14782  mertens  15934  aleph1re  16293  dvdslelem  16357  3dvdsdec  16380  3dvds2dec  16381  divalglem5  16445  ndvdsi  16460  bitsfzo  16481  absproddvds  16664  prmfac1  16767  prm23lt5  16861  dec2dvds  17110  dec5dvds2  17112  prmlem0  17153  dprd0  20075  ablfac1lem  20112  minveclem3b  25481  minveclem6  25487  minveclem7  25488  ioombl1lem4  25615  sinhalfpilem  26523  sincosq1lem  26557  sincosq1sgn  26558  sincosq2sgn  26559  sincosq3sgn  26560  sincosq4sgn  26561  bposlem6  27351  gausslemma2dlem1a  27427  2lgsoddprmlem3  27476  nosupinfsep  27795  addscut  28029  slt0neg2d  28101  mulscut  28176  abssneg  28289  elnnzs  28405  lfgrwlkprop  29723  konigsberglem4  30287  frgrwopreglem2  30345  avril1  30495  minvecolem5  30913  minvecolem6  30914  minvecolem7  30915  bcsiALT  31211  pjdifnormii  31715  cvexchi  32401  fldext2chn  33719  ballotlem4  34463  bnj110  34834  wsuclb  35792  dalem18  39638  dalem48  39677  cdlemblem  39750  cdleme7ga  40205  cdlemg27b  40653  frege116  43941  frege120  43945  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  hoidmv1lelem3  46514  hoidmvlelem3  46518  hoidmvle  46521  257prm  47435  fmtno4prmfac  47446  fmtno4nprmfac193  47448  flsqrt5  47468  139prmALT  47470  31prm  47471  127prm  47473  lighneallem2  47480  stgoldbwt  47650  nnsum3primesle9  47668  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  lincdifsn  48153  lindslinindsimp1  48186  lindslinindsimp2lem5  48191  lindslinindsimp2  48192  fldivexpfllog2  48299  nnlog2ge0lt1  48300  blen1b  48322  resum2sqorgt0  48443