Theorem breq2i 5115

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  breqtri  5132  en1  8995  sdom1  9189  enp1i  9224  enp1iOLD  9225  pm54.43  9954  addclprlem2  10970  map2psrpr  11063  lt0neg2  11685  le0neg2  11687  recgt1  12079  inelr  12176  addltmul  12418  nn0lt2  12597  3halfnz  12613  xlt0neg2  13180  xle0neg2  13182  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  hashen1  14335  swrdccatin2  14694  pfxccat3  14699  mertens  15852  aleph1re  16213  dvdslelem  16279  3dvdsdec  16302  3dvds2dec  16303  divalglem5  16367  ndvdsi  16382  bitsfzo  16405  absproddvds  16587  prmfac1  16690  prm23lt5  16785  dec2dvds  17034  dec5dvds2  17036  prmlem0  17076  dprd0  19963  ablfac1lem  20000  minveclem3b  25328  minveclem6  25334  minveclem7  25335  ioombl1lem4  25462  sinhalfpilem  26372  sincosq1lem  26406  sincosq1sgn  26407  sincosq2sgn  26408  sincosq3sgn  26409  sincosq4sgn  26410  bposlem6  27200  gausslemma2dlem1a  27276  2lgsoddprmlem3  27325  nosupinfsep  27644  addscut  27885  slt0neg2d  27957  mulscut  28035  abssneg  28149  elnnzs  28289  lfgrwlkprop  29615  konigsberglem4  30184  frgrwopreglem2  30242  avril1  30392  minvecolem5  30810  minvecolem6  30811  minvecolem7  30812  bcsiALT  31108  pjdifnormii  31612  cvexchi  32298  fldext2chn  33718  ballotlem4  34490  bnj110  34848  wsuclb  35816  dalem18  39675  dalem48  39714  cdlemblem  39787  cdleme7ga  40242  cdlemg27b  40690  sn-inelr  42475  frege116  43968  frege120  43972  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  hoidmv1lelem3  46591  hoidmvlelem3  46595  hoidmvle  46598  257prm  47559  fmtno4prmfac  47570  fmtno4nprmfac193  47572  flsqrt5  47592  139prmALT  47594  31prm  47595  127prm  47597  lighneallem2  47604  stgoldbwt  47774  nnsum3primesle9  47792  wtgoldbnnsum4prm  47800  bgoldbnnsum3prm  47802  lincdifsn  48410  lindslinindsimp1  48443  lindslinindsimp2lem5  48448  lindslinindsimp2  48449  fldivexpfllog2  48551  nnlog2ge0lt1  48552  blen1b  48574  resum2sqorgt0  48695