Theorem breq2i 5074

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

Syntax hints:   ↔ wb 208   = wceq 1537   class class class wbr 5066

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  breqtri  5091  en1  8576  snnen2o  8707  enp1i  8753  pm54.43  9429  addclprlem2  10439  map2psrpr  10532  lt0neg2  11147  le0neg2  11149  recgt1  11536  addltmul  11874  nn0lt2  12046  3halfnz  12062  xlt0neg2  12614  xle0neg2  12616  iccshftr  12873  iccshftl  12875  iccdil  12877  icccntr  12879  hashen1  13732  swrdccatin2  14091  pfxccat3  14096  mertens  15242  aleph1re  15598  dvdslelem  15659  3dvdsdec  15681  3dvds2dec  15682  divalglem5  15748  ndvdsi  15763  bitsfzo  15784  absproddvds  15961  prmfac1  16063  prm23lt5  16151  dec2dvds  16399  dec5dvds2  16401  prmlem0  16439  dprd0  19153  ablfac1lem  19190  minveclem3b  24031  minveclem6  24037  minveclem7  24038  ioombl1lem4  24162  sinhalfpilem  25049  sincosq1lem  25083  sincosq1sgn  25084  sincosq2sgn  25085  sincosq3sgn  25086  sincosq4sgn  25087  bposlem6  25865  gausslemma2dlem1a  25941  2lgsoddprmlem3  25990  lfgrwlkprop  27469  konigsberglem4  28034  frgrwopreglem2  28092  avril1  28242  minvecolem5  28658  minvecolem6  28659  minvecolem7  28660  bcsiALT  28956  pjdifnormii  29460  cvexchi  30146  ballotlem4  31756  bnj110  32130  wsuclb  33115  dalem18  36832  dalem48  36871  cdlemblem  36944  cdleme7ga  37399  cdlemg27b  37847  frege116  40374  frege120  40378  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  hoidmv1lelem3  42924  hoidmvlelem3  42928  hoidmvle  42931  257prm  43772  fmtno4prmfac  43783  fmtno4nprmfac193  43785  flsqrt5  43806  139prmALT  43808  31prm  43809  127prm  43812  lighneallem2  43820  stgoldbwt  43990  nnsum3primesle9  44008  wtgoldbnnsum4prm  44016  bgoldbnnsum3prm  44018  lincdifsn  44528  lindslinindsimp1  44561  lindslinindsimp2lem5  44566  lindslinindsimp2  44567  fldivexpfllog2  44674  nnlog2ge0lt1  44675  blen1b  44697  resum2sqorgt0  44745