Theorem breq2 4038

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

Assertion

Ref	Expression
breq2	|- ( A = B -> ( C R A <-> C R B ) )

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 3810	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2265	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4035	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4035	. 2 |- ( C R B <-> <. C , B >. e. R )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( C R A <-> C R B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   e. wcel 2167   <.cop 3626   class class class wbr 4034

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  breq12  4039  breq2i  4042  breq2d  4046  nbrne1  4053  brralrspcev  4092  brimralrspcev  4093  pocl  4339  swopolem  4341  swopo  4342  sowlin  4356  sotricim  4359  sotritrieq  4361  seex  4371  frind  4388  wetriext  4614  vtoclr  4712  posng  4736  brcog  4834  brcogw  4836  opelcnvg  4847  dfdmf  4860  breldmg  4873  dfrnf  4908  dmcoss  4936  resieq  4957  dfres2  4999  elimag  5014  elrelimasn  5036  elimasn  5037  intirr  5057  poirr2  5063  poltletr  5071  dffun6f  5272  dffun4f  5275  fun11  5326  brprcneu  5554  fv3  5584  tz6.12c  5591  relelfvdm  5593  funbrfv  5602  fnbrfvb  5604  funfvdm2f  5629  fndmdif  5670  dff3im  5710  fmptco  5731  foeqcnvco  5840  isorel  5858  isocnv  5861  isotr  5866  isopolem  5872  isosolem  5874  f1oiso  5876  f1oiso2  5877  caovordig  6093  caovordg  6095  caovord  6099  caofrss  6171  caoftrn  6172  poxp  6299  tposoprab  6347  ertr  6616  ecopovsym  6699  ecopovtrn  6700  ecopovsymg  6702  ecopovtrng  6703  th3qlem2  6706  domeng  6820  eqeng  6834  snfig  6882  nneneq  6927  nnfi  6942  ssfilem  6945  domfiexmid  6948  dif1enen  6950  diffitest  6957  findcard  6958  findcard2  6959  findcard2s  6960  diffisn  6963  tridc  6969  fimax2gtrilemstep  6970  inffiexmid  6976  unsnfi  6989  fiintim  7001  fisseneq  7004  isbth  7042  supmoti  7068  eqsupti  7071  supubti  7074  suplubti  7075  suplub2ti  7076  supmaxti  7079  supsnti  7080  isotilem  7081  isoti  7082  supisolem  7083  supisoex  7084  cardcl  7259  isnumi  7260  cardval3ex  7263  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  exmidapne  7343  nqtri3or  7480  ltsonq  7482  ltanqg  7484  ltmnqg  7485  ltexnqq  7492  nsmallnqq  7496  subhalfnqq  7498  ltbtwnnqq  7499  prarloclemarch2  7503  nqnq0pi  7522  prcdnql  7568  prcunqu  7569  prnminu  7573  genpcdl  7603  genprndl  7605  genprndu  7606  genpdisj  7607  nqprm  7626  nqprrnd  7627  nqprdisj  7628  nqprloc  7629  nqprlu  7631  nqprl  7635  addnqprlemru  7642  addnqprlemfl  7643  addnqprlemfu  7644  mulnqprlemru  7658  mulnqprlemfl  7659  mulnqprlemfu  7660  1idpru  7675  ltnqpr  7677  ltnqpri  7678  prplnqu  7704  recexprlemelu  7707  recexprlemm  7708  recexprlemloc  7715  recexprlem1ssl  7717  recexprlemss1u  7720  cauappcvgprlemm  7729  cauappcvgprlemopu  7732  cauappcvgprlemupu  7733  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdfu  7738  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem2  7744  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemopu  7755  caucvgprlemupu  7756  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemcl  7760  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlem2  7764  caucvgprprlemelu  7770  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemnbj  7777  caucvgprprlemmu  7779  caucvgprprlemexbt  7790  caucvgprprlemaddq  7792  caucvgprprlem1  7793  caucvgprprlem2  7794  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  suplocexpr  7809  lttrsr  7846  ltsosr  7848  ltasrg  7854  recexgt0sr  7857  mulgt0sr  7862  aptisr  7863  mulextsr1  7865  srpospr  7867  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  caucvgsr  7886  map2psrprg  7889  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  axprecex  7964  axpre-ltwlin  7967  axpre-lttrn  7968  axpre-apti  7969  axpre-ltadd  7970  axpre-mulgt0  7971  axpre-mulext  7972  axcaucvglemcau  7982  axcaucvglemres  7983  axcaucvg  7984  axpre-suploclemres  7985  axpre-suploc  7986  ltxrlt  8109  lttri3  8123  ltne  8128  eqle  8135  ltordlem  8526  reapti  8623  apreim  8647  squeeze0  8948  lbreu  8989  lble  8991  suprleubex  8998  sup3exmid  9001  nnge1  9030  nn2ge  9040  nn1gt1  9041  nnsub  9046  nominpos  9246  nn0ge0  9291  elnnnn0b  9310  nn0ge2m1nn  9326  zdclt  9420  suprzclex  9441  peano2uz2  9450  peano5uzti  9451  dfuzi  9453  uzind  9454  uzind3  9456  eluz1  9622  uzind4  9679  indstr  9684  supinfneg  9686  infsupneg  9687  infregelbex  9689  indstr2  9700  ublbneg  9704  irrmulap  9739  elpq  9740  elpqb  9741  elrp  9747  mnfltxr  9878  nn0pnfge0  9883  xrltnsym  9885  xrlttr  9887  xrltso  9888  xrlttri3  9889  xrltne  9905  ngtmnft  9909  nmnfgt  9910  xrrebnd  9911  z2ge  9918  xltnegi  9927  xltadd1  9968  xsubge0  9973  xleaddadd  9979  ixxval  9988  elixx1  9989  elioo2  10013  iccid  10017  iccsupr  10058  repos  10062  fzval  10102  elfz1  10105  fzm1  10192  zsupcllemstep  10336  suprzubdc  10343  zsupssdc  10345  qdclt  10352  exbtwnzlemstep  10354  exbtwnzlemex  10356  qbtwnre  10363  qbtwnxr  10364  flval  10379  apbtwnz  10381  modqid2  10460  modqmuladdnn0  10477  exp3val  10650  expge0  10684  expge1  10685  nn0ltexp2  10818  facdiv  10847  facwordi  10849  hashinfom  10887  hashennn  10889  hashunlem  10913  zfz1iso  10950  wrdlen1  10989  fstwrdne0  10991  ovshftex  11001  shftfibg  11002  shftfib  11005  shftfn  11006  2shfti  11013  sqrt0rlem  11185  resqrexlemex  11207  rsqrmo  11209  resqrtcl  11211  rersqrtthlem  11212  sqrtsq  11226  cau3lem  11296  caubnd2  11299  maxleim  11387  maxabslemval  11390  maxleast  11395  maxleb  11398  fimaxre2  11409  minmax  11412  xrmaxleim  11426  xrmaxiflemval  11432  xrmaxaddlem  11442  xrminmax  11447  xrbdtri  11458  climi  11469  climeu  11478  climmo  11480  2clim  11483  addcn2  11492  mulcn2  11494  reccn2ap  11495  cn1lem  11496  summodc  11565  zsumdc  11566  fsum3  11569  cvgratz  11714  ntrivcvgap0  11731  prodmodc  11760  zproddc  11761  fprodseq  11765  fprodntrivap  11766  sinltxirr  11943  dvdsabsb  11992  0dvds  11993  alzdvds  12036  dvdsext  12037  fzo0dvdseq  12039  2tp1odd  12066  2teven  12069  divalglemnn  12100  divalglemeunn  12103  divalglemeuneg  12105  bitsinv1lem  12143  gcdval  12151  gcddvds  12155  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlemex  12193  bezoutlemeu  12199  bezoutlemsup  12201  dfgcd3  12202  bezout  12203  dvdsgcd  12204  dfgcd2  12206  dvdssq  12223  uzwodc  12229  nnwofdc  12230  lcmval  12256  lcmcllem  12260  dvdslcm  12262  lcmledvds  12263  lcmgcdlem  12270  lcmdvds  12272  coprmgcdb  12281  coprmdvds2  12286  cncongr1  12296  cncongr2  12297  isprm  12302  dvdsnprmd  12318  dvdsprm  12330  exprmfct  12331  isprm6  12340  prmexpb  12344  prmfac1  12345  rpexp  12346  sqrt2irr  12355  oddpwdclemdc  12366  oddpwdc  12367  sqpweven  12368  2sqpwodd  12369  sqne2sq  12370  nnoddn2prmb  12456  pceu  12489  pczpre  12491  pcdiv  12496  pcdvdsb  12514  difsqpwdvds  12532  pcmpt  12537  pcmptdvds  12539  oddprmdvds  12548  prmpwdvds  12549  infpnlem2  12554  oddennn  12634  evenennn  12635  exmidunben  12668  nninfdclemcl  12690  nninfdclemp1  12692  nninfdc  12695  infpn2  12698  eqgen  13433  zndvds  14281  znleval  14285  comet  14819  metcnpi  14835  metcnpi2  14836  metcnpi3  14837  addcncntoplem  14881  cncfi  14898  elcncf1di  14899  mulcncflem  14927  dedekindeulemuub  14937  dedekindeulemloc  14939  dedekindeulemlu  14941  dedekindeulemeu  14942  dedekindeu  14943  suplociccreex  14944  suplociccex  14945  dedekindicclemuub  14946  dedekindicclemloc  14948  dedekindicclemlu  14950  dedekindicclemeu  14951  dedekindicclemicc  14952  dedekindicc  14953  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemloc  14961  ivthinc  14963  ivthreinc  14965  dich0  14972  ivthdich  14973  limcimo  14985  cnplimclemr  14989  limccnp2lem  14996  limccoap  14998  eldvap  15002  logltb  15194  lgsdir  15360  lgsne0  15363  gausslemma2dlem0i  15382  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  2lgslem2  15417  2lgs  15429  2sqlem6  15445  2sqlem8  15448  2sqlem10  15450  sbthom  15757  trilpo  15774  trirec0  15775  apdiff  15779  reap0  15789  cndcap  15790  nconstwlpolem  15796  neapmkv  15799  neap0mkv  15800  ltlenmkv  15801