Theorem breq2 3759

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
breq2	⊢ (A = B → (𝐶𝑅A ↔ 𝐶𝑅B))

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 3541	. . 3 ⊢ (A = B → ⟨𝐶, A⟩ = ⟨𝐶, B⟩)
2	1	eleq1d 2103	. 2 ⊢ (A = B → (⟨𝐶, A⟩ ∈ 𝑅 ↔ ⟨𝐶, B⟩ ∈ 𝑅))
3		df-br 3756	. 2 ⊢ (𝐶𝑅A ↔ ⟨𝐶, A⟩ ∈ 𝑅)
4		df-br 3756	. 2 ⊢ (𝐶𝑅B ↔ ⟨𝐶, B⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 212	1 ⊢ (A = B → (𝐶𝑅A ↔ 𝐶𝑅B))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1242   ∈ wcel 1390  ⟨cop 3370   class class class wbr 3755

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756

This theorem is referenced by:  breq12  3760  breq2i  3763  breq2d  3767  nbrne1  3772  pocl  4031  swopolem  4033  swopo  4034  sowlin  4048  sotricim  4051  sotritrieq  4053  seex  4057  vtoclr  4331  posng  4355  brcog  4445  brcogw  4447  opelcnvg  4458  dfdmf  4471  breldmg  4484  dfrnf  4518  dmcoss  4544  resieq  4565  dfres2  4601  elimag  4615  elreimasng  4634  elimasn  4635  intirr  4654  poirr2  4660  poltletr  4668  dffun6f  4858  dffun4f  4861  fun11  4909  brprcneu  5114  fv3  5140  tz6.12c  5146  relelfvdm  5148  funbrfv  5155  fnbrfvb  5157  funfvdm2f  5181  fndmdif  5215  dff3im  5255  fmptco  5273  foeqcnvco  5373  isorel  5391  isocnv  5394  isotr  5399  isopolem  5404  isosolem  5406  f1oiso  5408  f1oiso2  5409  caovordig  5608  caovordg  5610  caovord  5614  caofrss  5677  caoftrn  5678  poxp  5794  tposoprab  5836  ertr  6057  ecopovsym  6138  ecopovtrn  6139  ecopovsymg  6141  ecopovtrng  6142  th3qlem2  6145  domeng  6169  eqeng  6182  snfig  6227  nnfi  6251  ssfiexmid  6254  nqtri3or  6380  ltsonq  6382  ltanqg  6384  ltmnqg  6385  ltexnqq  6391  nsmallnqq  6395  subhalfnqq  6397  ltbtwnnqq  6398  prarloclemarch2  6402  nqnq0pi  6421  prcdnql  6467  prcunqu  6468  prnminu  6472  genpcdl  6502  genprndl  6504  genprndu  6505  genpdisj  6506  nqprm  6525  nqprrnd  6526  nqprdisj  6527  nqprloc  6528  nqprlu  6530  nqprl  6533  addnqprlemru  6539  addnqprlemfl  6540  addnqprlemfu  6541  1idpru  6567  recexprlemelu  6595  recexprlemm  6596  recexprlemloc  6603  recexprlem1ssl  6605  recexprlemss1u  6608  cauappcvgprlemm  6617  cauappcvgprlemopu  6620  cauappcvgprlemupu  6621  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdfu  6626  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem2  6632  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemm  6639  caucvgprlemopu  6642  caucvgprlemupu  6643  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemcl  6647  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem2  6651  lttrsr  6690  ltsosr  6692  ltasrg  6698  recexgt0sr  6701  mulgt0sr  6704  aptisr  6705  mulextsr1  6707  axprecex  6764  axpre-ltwlin  6767  axpre-lttrn  6768  axpre-apti  6769  axpre-ltadd  6770  axpre-mulgt0  6771  axpre-mulext  6772  ltxrlt  6882  lttri3  6895  ltne  6900  eqle  6906  reapti  7363  apreim  7387  squeeze0  7651  nnge1  7718  nn2ge  7727  nn1gt1  7728  nnsub  7733  nominpos  7939  nn0ge0  7983  elnnnn0b  8002  nn0ge2m1nn  8018  zdclt  8094  peano2uz2  8121  peano5uzti  8122  dfuzi  8124  uzind  8125  uzind3  8127  eluz1  8253  uzind4  8307  indstr  8312  indstr2  8322  ublbneg  8324  elrp  8360  mnfltxr  8477  nn0pnfge0  8482  xrltnsym  8484  xrlttr  8486  xrltso  8487  xrlttri3  8488  xrltne  8499  ngtmnft  8501  xrrebnd  8502  z2ge  8509  xltnegi  8518  ixxval  8535  elixx1  8536  elioo2  8560  iccid  8564  iccsupr  8605  repos  8609  fzval  8646  elfz1  8649  fzm1  8732  expival  8911  expge0  8945  expge1  8946  sqrt0rlem  9212  sqrtsq  9214