Theorem breq2i 3875

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

Syntax hints:   ↔ wb 104   = wceq 1296   class class class wbr 3867

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475  df-br 3868

This theorem is referenced by:  breqtri  3890  en1  6596  snnen2og  6655  1nen2  6657  pm54.43  6915  caucvgprprlemval  7344  caucvgprprlemmu  7351  caucvgsr  7444  pitonnlem1  7479  lt0neg2  8044  le0neg2  8046  negap0  8203  recexaplem2  8218  recgt1  8455  crap0  8516  addltmul  8750  nn0lt10b  8925  nn0lt2  8926  3halfnz  8942  xlt0neg2  9405  xle0neg2  9407  iccshftr  9560  iccshftl  9562  iccdil  9564  icccntr  9566  fihashen1  10322  cjap0  10456  abs00ap  10610  xrmaxiflemval  10793  mertenslem2  11079  mertensabs  11080  3dvdsdec  11292  3dvds2dec  11293  ndvdsi  11360  3prm  11537  prmfac1  11558