Theorem breq2i 3932

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

Syntax hints:   ↔ wb 104   = wceq 1331   class class class wbr 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-v 2683  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531  df-br 3925

This theorem is referenced by:  breqtri  3948  en1  6686  snnen2og  6746  1nen2  6748  pm54.43  7039  caucvgprprlemval  7489  caucvgprprlemmu  7496  caucvgsr  7603  pitonnlem1  7646  lt0neg2  8224  le0neg2  8226  negap0  8385  recexaplem2  8406  recgt1  8648  crap0  8709  addltmul  8949  nn0lt10b  9124  nn0lt2  9125  3halfnz  9141  xlt0neg2  9615  xle0neg2  9617  iccshftr  9770  iccshftl  9772  iccdil  9774  icccntr  9776  fihashen1  10538  cjap0  10672  abs00ap  10827  xrmaxiflemval  11012  mertenslem2  11298  mertensabs  11299  3dvdsdec  11551  3dvds2dec  11552  ndvdsi  11619  3prm  11798  prmfac1  11819  sinhalfpilem  12861  sincosq1lem  12895  sincosq1sgn  12896  sincosq2sgn  12897  sincosq3sgn  12898  sincosq4sgn  12899