Theorem breq2i 4012

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

Syntax hints:   ↔ wb 105   = wceq 1353   class class class wbr 4004

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005

This theorem is referenced by:  breqtri  4029  en1  6799  snnen2og  6859  1nen2  6861  pm54.43  7189  caucvgprprlemval  7687  caucvgprprlemmu  7694  caucvgsr  7801  pitonnlem1  7844  lt0neg2  8426  le0neg2  8428  negap0  8587  recexaplem2  8609  recgt1  8854  crap0  8915  addltmul  9155  nn0lt10b  9333  nn0lt2  9334  3halfnz  9350  xlt0neg2  9839  xle0neg2  9841  iccshftr  9994  iccshftl  9996  iccdil  9998  icccntr  10000  fihashen1  10779  cjap0  10916  abs00ap  11071  xrmaxiflemval  11258  mertenslem2  11544  mertensabs  11545  3dvdsdec  11870  3dvds2dec  11871  ndvdsi  11938  3prm  12128  prmfac1  12152  prm23lt5  12263  sinhalfpilem  14215  sincosq1lem  14249  sincosq1sgn  14250  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  logrpap0b  14300  2lgsoddprmlem3  14462