Theorem breq2i 5155

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

Syntax hints:   ↔ wb 205   = wceq 1542   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  breqtri  5172  en1  9017  en1OLD  9018  snnen2oOLD  9223  sdom1  9238  enp1i  9275  enp1iOLD  9276  pm54.43  9992  addclprlem2  11008  map2psrpr  11101  lt0neg2  11717  le0neg2  11719  recgt1  12106  addltmul  12444  nn0lt2  12621  3halfnz  12637  xlt0neg2  13195  xle0neg2  13197  iccshftr  13459  iccshftl  13461  iccdil  13463  icccntr  13465  hashen1  14326  swrdccatin2  14675  pfxccat3  14680  mertens  15828  aleph1re  16184  dvdslelem  16248  3dvdsdec  16271  3dvds2dec  16272  divalglem5  16336  ndvdsi  16351  bitsfzo  16372  absproddvds  16550  prmfac1  16654  prm23lt5  16743  dec2dvds  16992  dec5dvds2  16994  prmlem0  17035  dprd0  19893  ablfac1lem  19930  minveclem3b  24927  minveclem6  24933  minveclem7  24934  ioombl1lem4  25060  sinhalfpilem  25955  sincosq1lem  25989  sincosq1sgn  25990  sincosq2sgn  25991  sincosq3sgn  25992  sincosq4sgn  25993  bposlem6  26772  gausslemma2dlem1a  26848  2lgsoddprmlem3  26897  nosupinfsep  27215  addscut  27442  slt0neg2d  27505  mulscut  27568  lfgrwlkprop  28924  konigsberglem4  29488  frgrwopreglem2  29546  avril1  29696  minvecolem5  30112  minvecolem6  30113  minvecolem7  30114  bcsiALT  30410  pjdifnormii  30914  cvexchi  31600  ballotlem4  33435  bnj110  33807  wsuclb  34738  dalem18  38490  dalem48  38529  cdlemblem  38602  cdleme7ga  39057  cdlemg27b  39505  frege116  42663  frege120  42667  ioodvbdlimc1lem2  44583  ioodvbdlimc2lem  44585  hoidmv1lelem3  45244  hoidmvlelem3  45248  hoidmvle  45251  257prm  46164  fmtno4prmfac  46175  fmtno4nprmfac193  46177  flsqrt5  46197  139prmALT  46199  31prm  46200  127prm  46202  lighneallem2  46209  stgoldbwt  46379  nnsum3primesle9  46397  wtgoldbnnsum4prm  46405  bgoldbnnsum3prm  46407  lincdifsn  47007  lindslinindsimp1  47040  lindslinindsimp2lem5  47045  lindslinindsimp2  47046  fldivexpfllog2  47153  nnlog2ge0lt1  47154  blen1b  47176  resum2sqorgt0  47297