Theorem breq2i 3989

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

Syntax hints:   ↔ wb 104   = wceq 1343   class class class wbr 3981

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-br 3982

This theorem is referenced by:  breqtri  4006  en1  6761  snnen2og  6821  1nen2  6823  pm54.43  7142  caucvgprprlemval  7625  caucvgprprlemmu  7632  caucvgsr  7739  pitonnlem1  7782  lt0neg2  8363  le0neg2  8365  negap0  8524  recexaplem2  8545  recgt1  8788  crap0  8849  addltmul  9089  nn0lt10b  9267  nn0lt2  9268  3halfnz  9284  xlt0neg2  9771  xle0neg2  9773  iccshftr  9926  iccshftl  9928  iccdil  9930  icccntr  9932  fihashen1  10708  cjap0  10845  abs00ap  11000  xrmaxiflemval  11187  mertenslem2  11473  mertensabs  11474  3dvdsdec  11798  3dvds2dec  11799  ndvdsi  11866  3prm  12056  prmfac1  12080  prm23lt5  12191  sinhalfpilem  13312  sincosq1lem  13346  sincosq1sgn  13347  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  logrpap0b  13397