Theorem breq2i 4094

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

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

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  breqtri  4111  en1  6968  snnen2og  7040  1nen2  7042  pm54.43  7386  caucvgprprlemval  7898  caucvgprprlemmu  7905  caucvgsr  8012  pitonnlem1  8055  lt0neg2  8639  le0neg2  8641  negap0  8800  recexaplem2  8822  recgt1  9067  crap0  9128  addltmul  9371  nn0lt10b  9550  nn0lt2  9551  3halfnz  9567  xlt0neg2  10064  xle0neg2  10066  iccshftr  10219  iccshftl  10221  iccdil  10223  icccntr  10225  fihashen1  11051  swrdccatin2  11300  pfxccat3  11305  cjap0  11458  abs00ap  11613  xrmaxiflemval  11801  mertenslem2  12087  mertensabs  12088  3dvdsdec  12416  3dvds2dec  12417  ndvdsi  12484  bitsfzo  12506  3prm  12690  prmfac1  12714  prm23lt5  12826  dec2dvds  12974  dec5dvds2  12976  sinhalfpilem  15505  sincosq1lem  15539  sincosq1sgn  15540  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  logrpap0b  15590  gausslemma2dlem1a  15777  2lgsoddprmlem3  15830