Theorem breq2i 4091

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

Syntax hints:   ↔ wb 105   = wceq 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breqtri  4108  en1  6959  snnen2og  7028  1nen2  7030  pm54.43  7374  caucvgprprlemval  7886  caucvgprprlemmu  7893  caucvgsr  8000  pitonnlem1  8043  lt0neg2  8627  le0neg2  8629  negap0  8788  recexaplem2  8810  recgt1  9055  crap0  9116  addltmul  9359  nn0lt10b  9538  nn0lt2  9539  3halfnz  9555  xlt0neg2  10047  xle0neg2  10049  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  fihashen1  11033  swrdccatin2  11277  pfxccat3  11282  cjap0  11434  abs00ap  11589  xrmaxiflemval  11777  mertenslem2  12063  mertensabs  12064  3dvdsdec  12392  3dvds2dec  12393  ndvdsi  12460  bitsfzo  12482  3prm  12666  prmfac1  12690  prm23lt5  12802  dec2dvds  12950  dec5dvds2  12952  sinhalfpilem  15481  sincosq1lem  15515  sincosq1sgn  15516  sincosq2sgn  15517  sincosq3sgn  15518  sincosq4sgn  15519  logrpap0b  15566  gausslemma2dlem1a  15753  2lgsoddprmlem3  15806