Theorem breq1 4086

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 3857	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	eleq1d 2298	. 2 |- ( A = B -> ( <. A , C >. e. R <-> <. B , C >. e. R ) )
3		df-br 4084	. 2 |- ( A R C <-> <. A , C >. e. R )
4		df-br 4084	. 2 |- ( B R C <-> <. B , C >. e. R )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( A R C <-> B R C ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1395   e. wcel 2200   <.cop 3669   class class class wbr 4083

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breq12  4088  breq1i  4090  breq1d  4093  nbrne2  4103  brab1  4131  pocl  4394  swopolem  4396  swopo  4397  issod  4410  sowlin  4411  sotritrieq  4416  frirrg  4441  wetriext  4669  vtoclr  4767  brcog  4889  brcogw  4891  opelcnvg  4902  dfdmf  4916  eldmg  4918  dfrnf  4965  dfres2  5057  imasng  5093  coi1  5244  dffun6f  5331  funmo  5333  fun11  5388  fveq2  5627  funfveu  5640  sefvex  5648  nfunsn  5664  fvmptss2  5709  f1ompt  5786  fmptco  5801  dff13  5892  foeqcnvco  5914  isorel  5932  isocnv  5935  isotr  5940  isoini  5942  isopolem  5946  isosolem  5948  f1oiso  5950  f1oiso2  5951  caovordig  6171  caovordg  6173  caovord3d  6176  caovord  6177  caovord3  6179  caofrss  6250  caoftrn  6251  poxp  6378  brtpos2  6397  rntpos  6403  tpostpos  6410  ertr  6695  ecopovsym  6778  ecopovtrn  6779  ecopovsymg  6781  ecopovtrng  6782  th3qlem2  6785  isfi  6912  en0  6947  en1  6951  en1bg  6952  endisj  6983  xpcomco  6985  dom0  6999  ssenen  7012  nneneq  7018  domfiexmid  7040  findcard  7050  findcard2  7051  findcard2s  7052  isinfinf  7059  tridc  7061  fimax2gtrilemstep  7062  fimax2gtri  7063  fiintim  7093  fisseneq  7096  en1eqsnbi  7116  isbth  7134  supmoti  7160  eqsupti  7163  supubti  7166  suplubti  7167  supsnti  7172  isotilem  7173  isoti  7174  supisolem  7175  supisoex  7176  infminti  7194  isnumi  7354  cardval3ex  7357  oncardval  7358  cardonle  7359  en2prde  7366  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  exmidapne  7446  nqtri3or  7583  ltsonq  7585  ltanqg  7587  ltmnqg  7588  ltexnqq  7595  subhalfnqq  7601  ltbtwnnqq  7602  archnqq  7604  nqnq0pi  7625  prcdnql  7671  prcunqu  7672  prnmaxl  7675  genpcuu  7707  genprndl  7708  genprndu  7709  nqprm  7729  nqprrnd  7730  nqprdisj  7731  nqprloc  7732  nqpru  7739  addnqprlemrl  7744  addnqprlemfl  7746  addnqprlemfu  7747  prmuloc2  7754  mulnqprlemrl  7760  mulnqprlemfl  7762  mulnqprlemfu  7763  1idprl  7777  ltnqpr  7780  ltnqpri  7781  prplnqu  7807  recexprlemell  7809  recexprlemm  7811  recexprlemdisj  7817  recexprlemloc  7818  recexprlem1ssu  7821  recexprlemss1l  7822  aptiprlemu  7827  archpr  7830  cauappcvgprlemm  7832  cauappcvgprlemladdfl  7842  cauappcvgprlem2  7847  cauappcvgpr  7849  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemcl  7863  caucvgprlem2  7867  caucvgpr  7869  caucvgprprlemelu  7873  caucvgprprlemcbv  7874  caucvgprprlemval  7875  caucvgprprlemnbj  7880  caucvgprprlemmu  7882  caucvgprprlemopu  7886  caucvgprprlemexbt  7893  caucvgprprlemaddq  7895  caucvgprprlem1  7896  caucvgprprlem2  7897  caucvgprpr  7899  suplocexprlemmu  7905  suplocexprlemloc  7908  suplocexpr  7912  lttrsr  7949  ltsosr  7951  1ne0sr  7953  ltasrg  7957  aptisr  7966  mulextsr1  7968  archsr  7969  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  caucvgsr  7989  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  axpre-ltwlin  8070  axpre-lttrn  8071  axpre-apti  8072  axpre-ltadd  8073  axpre-mulext  8075  axcaucvglemcau  8085  axcaucvglemres  8086  axcaucvg  8087  axpre-suploclemres  8088  axpre-suploc  8089  ltxrlt  8212  lttri3  8226  ltordlem  8629  lt0ne0d  8660  reapti  8726  apreim  8750  apsscn  8794  recexap  8800  lbreu  9092  lble  9094  suprleubex  9101  sup3exmid  9104  nnsub  9149  nominpos  9349  nn0n0n1ge2b  9526  zextle  9538  fzind  9562  btwnz  9566  uzval  9724  supinfneg  9790  infsupneg  9791  infregelbex  9793  ublbneg  9808  lbzbi  9811  qreccl  9837  xrltnsym  9989  xrlttr  9991  xrltso  9992  xrlttri3  9993  nltpnft  10010  npnflt  10011  xrrebnd  10015  xltnegi  10031  xnn0lenn0nn0  10061  xsubge0  10077  xlesubadd  10079  xleaddadd  10083  ixxval  10092  elixx1  10093  elioo2  10117  iccid  10121  fzval  10206  elfz1  10209  zsupcllemstep  10449  suprzubdc  10456  zsupssdc  10458  qtri3or  10460  exbtwnzlemstep  10467  exbtwnzlemshrink  10468  exbtwnzlemex  10469  exbtwnz  10470  rebtwn2zlemstep  10472  rebtwn2zlemshrink  10473  rebtwn2z  10474  qbtwnre  10476  qbtwnxr  10477  flval  10492  flqlelt  10496  flqbi  10510  flqeqceilz  10540  modqid2  10573  seq3f1olemqsum  10735  seq3f1oleml  10738  seq3f1o  10739  seqf1oglem2  10742  expcl2lemap  10773  expclzaplem  10785  expclzap  10786  expap0i  10793  nn0ltexp2  10931  hashinfuni  10999  hashennnuni  11001  hashunlem  11026  zfz1isolemiso  11061  zfz1isolem1  11062  zfz1iso  11063  absle  11600  maxleast  11724  rexanre  11731  rexico  11732  fimaxre2  11738  minmax  11741  xrmaxltsup  11769  xrminmax  11776  climshft  11815  reccn2ap  11824  summodclem3  11891  summodclem2a  11892  summodc  11894  zsumdc  11895  fsum3  11898  fsum3cvg3  11907  fsumcl2lem  11909  fsumadd  11917  sumsnf  11920  fsummulc2  11959  isumlessdc  12007  cvgratz  12043  mertenslemi1  12046  ntrivcvgap0  12060  prodmodclem3  12086  prodmodclem2a  12087  prodmodc  12089  zproddc  12090  fprodseq  12094  fprodntrivap  12095  fprodmul  12102  prodsnf  12103  absdvdsb  12320  zdvdsdc  12323  dvdsabseq  12358  dvdsdivcl  12361  dvdsext  12366  divalglemnn  12429  divalglemeunn  12432  divalglemeuneg  12434  divalgmod  12438  ndvdssub  12441  gcdsupex  12478  gcdsupcl  12479  gcddvds  12484  dvdslegcd  12485  bezoutlemmain  12519  bezoutlemex  12522  bezoutlemzz  12523  bezoutlemmo  12527  bezoutlemeu  12528  bezoutlemle  12529  bezoutlemsup  12530  dfgcd3  12531  dfgcd2  12535  gcdzeq  12543  dvdssq  12552  nnwodc  12557  uzwodc  12558  nnwofdc  12559  nn0seqcvgd  12563  algcvgblem  12571  lcmval  12585  lcmdvds  12601  lcmgcdeq  12605  coprmgcdb  12610  ncoprmgcdne1b  12611  coprmdvds1  12613  1nprm  12636  1idssfct  12637  isprm2lem  12638  isprm2  12639  dvdsprime  12644  nprm  12645  3prm  12650  dvdsprm  12659  exprmfct  12660  isprm5lem  12663  isprm5  12664  coprm  12666  sqrt2irr  12684  dvdsfi  12761  phisum  12763  odzval  12764  pythagtriplem4  12791  pc2dvds  12853  pcprmpw2  12856  pcprmpw  12857  dvdsprmpweqle  12860  oddprmdvds  12877  prmpwdvds  12878  pockthg  12880  1arith  12890  exmidunben  12997  nninfdclemcl  13019  nninfdclemp1  13021  nninfdc  13024  imasaddfnlemg  13347  cnfldui  14553  znleval  14617  ssblex  15105  comet  15173  bdmopn  15178  reopnap  15220  divcnap  15239  cdivcncfap  15278  cnopnap  15285  divcncfap  15288  maxcncf  15289  mincncf  15290  dedekindeulemuub  15291  dedekindeulemloc  15293  dedekindeulemlu  15295  dedekindeulemeu  15296  dedekindeu  15297  suplociccreex  15298  dedekindicclemuub  15300  dedekindicclemloc  15302  dedekindicclemlu  15304  dedekindicclemeu  15305  dedekindicclemicc  15306  dedekindicc  15307  ivthinclemlopn  15310  ivthinclemlr  15311  ivthinclemuopn  15312  ivthinclemur  15313  ivthinclemloc  15315  ivthinc  15317  ivthreinc  15319  dich0  15326  ivthdich  15327  limcdifap  15336  limcimolemlt  15338  limccoap  15352  dvlemap  15354  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvcnp2cntop  15373  dvaddxxbr  15375  dvmulxxbr  15376  dvcoapbr  15381  dvcjbr  15382  dvrecap  15387  dveflem  15400  logltb  15548  2irrexpqap  15652  sgmnncl  15662  dvdsppwf1o  15663  mpodvdsmulf1o  15664  perfectlem2  15674  lgsmod  15705  lgsne0  15717  gausslemma2dlem4  15743  2sqlem6  15799  2sqlem8  15802  2sqlem10  15804  upgrm  15900  upgr1or2  15901  umgredg2en  15909  umgrbien  15910  upgr1elem1  15920  edgupgren  15939  edgumgren  15940  umgredgnlp  15950  edgusgren  15961  usgruspgrben  15984  wlkvtxiedg  16056  wlkvtxiedgg  16057  pw1nct  16369  sbthom  16394  trilpo  16411  trirec0  16412  reap0  16426  cndcap  16427  dcapnconst  16429  neapmkv  16436  neap0mkv  16437  ltlenmkv  16438