Theorem breq2i 4119

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

Syntax hints:   ↔ wb 105   = wceq 1398   class class class wbr 4111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-br 4112

This theorem is referenced by:  breqtri  4136  en1  7041  snnen2og  7115  1nen2  7117  pm54.43  7489  caucvgprprlemval  8005  caucvgprprlemmu  8012  caucvgsr  8119  pitonnlem1  8162  lt0neg2  8745  le0neg2  8747  negap0  8906  recexaplem2  8928  recgt1  9173  crap0  9234  addltmul  9477  nn0lt10b  9661  nn0lt2  9662  3halfnz  9678  xlt0neg2  10175  xle0neg2  10177  iccshftr  10330  iccshftl  10332  iccdil  10334  icccntr  10336  fihashen1  11166  swrdccatin2  11425  pfxccat3  11430  cjap0  11596  abs00ap  11751  xrmaxiflemval  11939  mertenslem2  12226  mertensabs  12227  3dvdsdec  12555  3dvds2dec  12556  ndvdsi  12623  bitsfzo  12645  3prm  12829  prmfac1  12853  prm23lt5  12965  dec2dvds  13113  dec5dvds2  13115  ballotfilem4  13159  sinhalfpilem  15673  sincosq1lem  15707  sincosq1sgn  15708  sincosq2sgn  15709  sincosq3sgn  15710  sincosq4sgn  15711  logrpap0b  15758  gausslemma2dlem1a  15948  2lgsoddprmlem3  16001  konigsberglem4  16503