Theorem breq1 3979

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

Assertion

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

Proof of Theorem breq1

Step	Hyp	Ref	Expression
1		opeq1 3752	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	eleq1d 2233	. 2 |- ( A = B -> ( <. A , C >. e. R <-> <. B , C >. e. R ) )
3		df-br 3977	. 2 |- ( A R C <-> <. A , C >. e. R )
4		df-br 3977	. 2 |- ( B R C <-> <. B , C >. e. R )
5	2, 3, 4	3bitr4g 222	1 |- ( A = B -> ( A R C <-> B R C ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1342   e. wcel 2135   <.cop 3573   class class class wbr 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579  df-br 3977

This theorem is referenced by:  breq12  3981  breq1i  3983  breq1d  3986  nbrne2  3996  brab1  4023  pocl  4275  swopolem  4277  swopo  4278  issod  4291  sowlin  4292  sotritrieq  4297  frirrg  4322  wetriext  4548  vtoclr  4646  brcog  4765  brcogw  4767  opelcnvg  4778  dfdmf  4791  eldmg  4793  dfrnf  4839  dfres2  4930  imasng  4963  coi1  5113  dffun6f  5195  funmo  5197  fun11  5249  fveq2  5480  funfveu  5493  sefvex  5501  nfunsn  5514  fvmptss2  5555  f1ompt  5630  fmptco  5645  dff13  5730  foeqcnvco  5752  isorel  5770  isocnv  5773  isotr  5778  isoini  5780  isopolem  5784  isosolem  5786  f1oiso  5788  f1oiso2  5789  caovordig  5998  caovordg  6000  caovord3d  6003  caovord  6004  caovord3  6006  caofrss  6068  caoftrn  6069  poxp  6191  brtpos2  6210  rntpos  6216  tpostpos  6223  ertr  6507  ecopovsym  6588  ecopovtrn  6589  ecopovsymg  6591  ecopovtrng  6592  th3qlem2  6595  isfi  6718  en0  6752  en1  6756  en1bg  6757  endisj  6781  xpcomco  6783  dom0  6795  ssenen  6808  nneneq  6814  domfiexmid  6835  findcard  6845  findcard2  6846  findcard2s  6847  isinfinf  6854  tridc  6856  fimax2gtrilemstep  6857  fimax2gtri  6858  fiintim  6885  fisseneq  6888  en1eqsnbi  6905  isbth  6923  supmoti  6949  eqsupti  6952  supubti  6955  suplubti  6956  supsnti  6961  isotilem  6962  isoti  6963  supisolem  6964  supisoex  6965  infminti  6983  isnumi  7129  cardval3ex  7132  oncardval  7133  cardonle  7134  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  nqtri3or  7328  ltsonq  7330  ltanqg  7332  ltmnqg  7333  ltexnqq  7340  subhalfnqq  7346  ltbtwnnqq  7347  archnqq  7349  nqnq0pi  7370  prcdnql  7416  prcunqu  7417  prnmaxl  7420  genpcuu  7452  genprndl  7453  genprndu  7454  nqprm  7474  nqprrnd  7475  nqprdisj  7476  nqprloc  7477  nqpru  7484  addnqprlemrl  7489  addnqprlemfl  7491  addnqprlemfu  7492  prmuloc2  7499  mulnqprlemrl  7505  mulnqprlemfl  7507  mulnqprlemfu  7508  1idprl  7522  ltnqpr  7525  ltnqpri  7526  prplnqu  7552  recexprlemell  7554  recexprlemm  7556  recexprlemdisj  7562  recexprlemloc  7563  recexprlem1ssu  7566  recexprlemss1l  7567  aptiprlemu  7572  archpr  7575  cauappcvgprlemm  7577  cauappcvgprlemladdfl  7587  cauappcvgprlem2  7592  cauappcvgpr  7594  caucvgprlemnkj  7598  caucvgprlemnbj  7599  caucvgprlemcl  7608  caucvgprlem2  7612  caucvgpr  7614  caucvgprprlemelu  7618  caucvgprprlemcbv  7619  caucvgprprlemval  7620  caucvgprprlemnbj  7625  caucvgprprlemmu  7627  caucvgprprlemopu  7631  caucvgprprlemexbt  7638  caucvgprprlemaddq  7640  caucvgprprlem1  7641  caucvgprprlem2  7642  caucvgprpr  7644  suplocexprlemmu  7650  suplocexprlemloc  7653  suplocexpr  7657  lttrsr  7694  ltsosr  7696  1ne0sr  7698  ltasrg  7702  aptisr  7711  mulextsr1  7713  archsr  7714  caucvgsrlemgt1  7727  caucvgsrlemoffres  7732  caucvgsr  7734  suplocsrlemb  7738  suplocsrlempr  7739  suplocsrlem  7740  axpre-ltwlin  7815  axpre-lttrn  7816  axpre-apti  7817  axpre-ltadd  7818  axpre-mulext  7820  axcaucvglemcau  7830  axcaucvglemres  7831  axcaucvg  7832  axpre-suploclemres  7833  axpre-suploc  7834  ltxrlt  7955  lttri3  7969  ltordlem  8371  lt0ne0d  8402  reapti  8468  apreim  8492  apsscn  8536  recexap  8541  lbreu  8831  lble  8833  suprleubex  8840  sup3exmid  8843  nnsub  8887  nominpos  9085  nn0n0n1ge2b  9261  zextle  9273  fzind  9297  btwnz  9301  uzval  9459  supinfneg  9524  infsupneg  9525  infregelbex  9527  ublbneg  9542  lbzbi  9545  qreccl  9571  xrltnsym  9720  xrlttr  9722  xrltso  9723  xrlttri3  9724  nltpnft  9741  npnflt  9742  xrrebnd  9746  xltnegi  9762  xnn0lenn0nn0  9792  xsubge0  9808  xlesubadd  9810  xleaddadd  9814  ixxval  9823  elixx1  9824  elioo2  9848  iccid  9852  fzval  9937  elfz1  9940  qtri3or  10168  exbtwnzlemstep  10173  exbtwnzlemshrink  10174  exbtwnzlemex  10175  exbtwnz  10176  rebtwn2zlemstep  10178  rebtwn2zlemshrink  10179  rebtwn2z  10180  qbtwnre  10182  qbtwnxr  10183  flval  10197  flqlelt  10201  flqbi  10215  flqeqceilz  10243  modqid2  10276  seq3f1olemqsum  10425  seq3f1oleml  10428  seq3f1o  10429  expcl2lemap  10457  expclzaplem  10469  expclzap  10470  expap0i  10477  nn0ltexp2  10612  hashinfuni  10679  hashennnuni  10681  hashunlem  10706  zfz1isolemiso  10738  zfz1isolem1  10739  zfz1iso  10740  absle  11017  maxleast  11141  rexanre  11148  rexico  11149  fimaxre2  11154  minmax  11157  xrmaxltsup  11185  xrminmax  11192  climshft  11231  reccn2ap  11240  summodclem3  11307  summodclem2a  11308  summodc  11310  zsumdc  11311  fsum3  11314  fsum3cvg3  11323  fsumcl2lem  11325  fsumadd  11333  sumsnf  11336  fsummulc2  11375  isumlessdc  11423  cvgratz  11459  mertenslemi1  11462  ntrivcvgap0  11476  prodmodclem3  11502  prodmodclem2a  11503  prodmodc  11505  zproddc  11506  fprodseq  11510  fprodntrivap  11511  fprodmul  11518  prodsnf  11519  absdvdsb  11735  zdvdsdc  11738  dvdsabseq  11770  dvdsdivcl  11773  dvdsext  11778  divalglemnn  11840  divalglemeunn  11843  divalglemeuneg  11845  divalgmod  11849  ndvdssub  11852  zsupcllemstep  11863  suprzubdc  11870  zsupssdc  11872  gcdsupex  11875  gcdsupcl  11876  gcddvds  11881  dvdslegcd  11882  bezoutlemmain  11916  bezoutlemex  11919  bezoutlemzz  11920  bezoutlemmo  11924  bezoutlemeu  11925  bezoutlemle  11926  bezoutlemsup  11927  dfgcd3  11928  dfgcd2  11932  gcdzeq  11940  dvdssq  11949  nn0seqcvgd  11952  algcvgblem  11960  lcmval  11974  lcmdvds  11990  lcmgcdeq  11994  coprmgcdb  11999  ncoprmgcdne1b  12000  coprmdvds1  12002  1nprm  12025  1idssfct  12026  isprm2lem  12027  isprm2  12028  dvdsprime  12033  nprm  12034  3prm  12039  dvdsprm  12048  exprmfct  12049  coprm  12053  sqrt2irr  12071  phisum  12149  odzval  12150  pythagtriplem4  12177  pc2dvds  12238  pcprmpw2  12241  pcprmpw  12242  dvdsprmpweqle  12245  oddprmdvds  12261  exmidunben  12296  nninfdclemcl  12320  nninfdclemp1  12322  nninfdc  12325  ssblex  12972  comet  13040  bdmopn  13045  reopnap  13079  divcnap  13096  cdivcncfap  13128  cnopnap  13135  dedekindeulemuub  13136  dedekindeulemloc  13138  dedekindeulemlu  13140  dedekindeulemeu  13141  dedekindeu  13142  suplociccreex  13143  dedekindicclemuub  13145  dedekindicclemloc  13147  dedekindicclemlu  13149  dedekindicclemeu  13150  dedekindicclemicc  13151  dedekindicc  13152  ivthinclemlopn  13155  ivthinclemlr  13156  ivthinclemuopn  13157  ivthinclemur  13158  ivthinclemloc  13160  ivthinc  13162  limcdifap  13172  limcimolemlt  13174  limccoap  13188  dvlemap  13190  dvidlemap  13201  dvcnp2cntop  13204  dvaddxxbr  13206  dvmulxxbr  13207  dvcoapbr  13212  dvcjbr  13213  dvrecap  13218  dveflem  13228  logltb  13336  2irrexpqap  13437  pw1nct  13717  sbthom  13739  trilpo  13756  trirec0  13757  reap0  13771  dcapnconst  13773  neapmkv  13780