Theorem breq1 3898

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 3671	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	eleq1d 2183	. 2 |- ( A = B -> ( <. A , C >. e. R <-> <. B , C >. e. R ) )
3		df-br 3896	. 2 |- ( A R C <-> <. A , C >. e. R )
4		df-br 3896	. 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 1314   e. wcel 1463   <.cop 3496   class class class wbr 3895

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-v 2659  df-un 3041  df-sn 3499  df-pr 3500  df-op 3502  df-br 3896

This theorem is referenced by:  breq12  3900  breq1i  3902  breq1d  3905  nbrne2  3913  brab1  3940  pocl  4185  swopolem  4187  swopo  4188  issod  4201  sowlin  4202  sotritrieq  4207  frirrg  4232  wetriext  4451  vtoclr  4547  brcog  4666  brcogw  4668  opelcnvg  4679  dfdmf  4692  eldmg  4694  dfrnf  4740  dfres2  4829  imasng  4862  coi1  5012  dffun6f  5094  funmo  5096  fun11  5148  fveq2  5375  funfveu  5388  sefvex  5396  nfunsn  5409  fvmptss2  5450  f1ompt  5525  fmptco  5540  dff13  5623  foeqcnvco  5645  isorel  5663  isocnv  5666  isotr  5671  isoini  5673  isopolem  5677  isosolem  5679  f1oiso  5681  f1oiso2  5682  caovordig  5890  caovordg  5892  caovord3d  5895  caovord  5896  caovord3  5898  caofrss  5960  caoftrn  5961  poxp  6083  brtpos2  6102  rntpos  6108  tpostpos  6115  ertr  6398  ecopovsym  6479  ecopovtrn  6480  ecopovsymg  6482  ecopovtrng  6483  th3qlem2  6486  isfi  6609  en0  6643  en1  6647  en1bg  6648  endisj  6671  xpcomco  6673  dom0  6685  ssenen  6698  nneneq  6704  domfiexmid  6725  findcard  6735  findcard2  6736  findcard2s  6737  isinfinf  6744  tridc  6746  fimax2gtrilemstep  6747  fimax2gtri  6748  fiintim  6770  fisseneq  6773  en1eqsnbi  6789  isbth  6807  supmoti  6832  eqsupti  6835  supubti  6838  suplubti  6839  supsnti  6844  isotilem  6845  isoti  6846  supisolem  6847  supisoex  6848  infminti  6866  isnumi  6988  cardval3ex  6991  oncardval  6992  cardonle  6993  exmidfodomrlemr  7006  exmidfodomrlemrALT  7007  nqtri3or  7152  ltsonq  7154  ltanqg  7156  ltmnqg  7157  ltexnqq  7164  subhalfnqq  7170  ltbtwnnqq  7171  archnqq  7173  nqnq0pi  7194  prcdnql  7240  prcunqu  7241  prnmaxl  7244  genpcuu  7276  genprndl  7277  genprndu  7278  nqprm  7298  nqprrnd  7299  nqprdisj  7300  nqprloc  7301  nqpru  7308  addnqprlemrl  7313  addnqprlemfl  7315  addnqprlemfu  7316  prmuloc2  7323  mulnqprlemrl  7329  mulnqprlemfl  7331  mulnqprlemfu  7332  1idprl  7346  ltnqpr  7349  ltnqpri  7350  prplnqu  7376  recexprlemell  7378  recexprlemm  7380  recexprlemdisj  7386  recexprlemloc  7387  recexprlem1ssu  7390  recexprlemss1l  7391  aptiprlemu  7396  archpr  7399  cauappcvgprlemm  7401  cauappcvgprlemladdfl  7411  cauappcvgprlem2  7416  cauappcvgpr  7418  caucvgprlemnkj  7422  caucvgprlemnbj  7423  caucvgprlemcl  7432  caucvgprlem2  7436  caucvgpr  7438  caucvgprprlemelu  7442  caucvgprprlemcbv  7443  caucvgprprlemval  7444  caucvgprprlemnbj  7449  caucvgprprlemmu  7451  caucvgprprlemopu  7455  caucvgprprlemexbt  7462  caucvgprprlemaddq  7464  caucvgprprlem1  7465  caucvgprprlem2  7466  caucvgprpr  7468  lttrsr  7505  ltsosr  7507  1ne0sr  7509  ltasrg  7513  aptisr  7521  mulextsr1  7523  archsr  7524  caucvgsrlemgt1  7537  caucvgsrlemoffres  7542  caucvgsr  7544  axpre-ltwlin  7618  axpre-lttrn  7619  axpre-apti  7620  axpre-ltadd  7621  axpre-mulext  7623  axcaucvglemcau  7633  axcaucvglemres  7634  axcaucvg  7635  ltxrlt  7754  lttri3  7767  ltordlem  8163  lt0ne0d  8194  reapti  8259  apreim  8283  recexap  8327  lbreu  8613  lble  8615  suprleubex  8622  sup3exmid  8625  nnsub  8669  nominpos  8861  nn0n0n1ge2b  9034  zextle  9046  fzind  9070  btwnz  9074  uzval  9230  supinfneg  9292  infsupneg  9293  ublbneg  9307  lbzbi  9310  qreccl  9336  xrltnsym  9472  xrlttr  9474  xrltso  9475  xrlttri3  9476  nltpnft  9490  npnflt  9491  xrrebnd  9495  xltnegi  9511  xnn0lenn0nn0  9541  xsubge0  9557  xlesubadd  9559  xleaddadd  9563  ixxval  9572  elixx1  9573  elioo2  9597  iccid  9601  fzval  9685  elfz1  9688  qtri3or  9913  exbtwnzlemstep  9918  exbtwnzlemshrink  9919  exbtwnzlemex  9920  exbtwnz  9921  rebtwn2zlemstep  9923  rebtwn2zlemshrink  9924  rebtwn2z  9925  qbtwnre  9927  qbtwnxr  9928  flval  9938  flqlelt  9942  flqbi  9956  flqeqceilz  9984  modqid2  10017  seq3f1olemqsum  10166  seq3f1oleml  10169  seq3f1o  10170  expcl2lemap  10198  expclzaplem  10210  expclzap  10211  expap0i  10218  hashinfuni  10416  hashennnuni  10418  hashunlem  10443  zfz1isolemiso  10475  zfz1isolem1  10476  zfz1iso  10477  absle  10753  maxleast  10877  rexanre  10884  rexico  10885  fimaxre2  10890  minmax  10893  xrmaxltsup  10919  xrminmax  10926  climshft  10965  reccn2ap  10974  summodclem3  11041  summodclem2a  11042  summodc  11044  zsumdc  11045  fsum3  11048  fsum3cvg3  11057  fsumcl2lem  11059  fsumadd  11067  sumsnf  11070  fsummulc2  11109  isumlessdc  11157  cvgratz  11193  mertenslemi1  11196  absdvdsb  11359  zdvdsdc  11362  dvdsabseq  11393  dvdsdivcl  11396  dvdsext  11401  divalglemnn  11463  divalglemeunn  11466  divalglemeuneg  11468  divalgmod  11472  ndvdssub  11475  zsupcllemstep  11486  gcdsupex  11494  gcdsupcl  11495  gcddvds  11500  dvdslegcd  11501  bezoutlemmain  11532  bezoutlemex  11535  bezoutlemzz  11536  bezoutlemmo  11540  bezoutlemeu  11541  bezoutlemle  11542  bezoutlemsup  11543  dfgcd3  11544  dfgcd2  11548  gcdzeq  11556  dvdssq  11565  nn0seqcvgd  11568  algcvgblem  11576  lcmval  11590  lcmdvds  11606  lcmgcdeq  11610  coprmgcdb  11615  ncoprmgcdne1b  11616  coprmdvds1  11618  1nprm  11641  1idssfct  11642  isprm2lem  11643  isprm2  11644  dvdsprime  11649  nprm  11650  3prm  11655  dvdsprm  11663  exprmfct  11664  coprm  11668  sqrt2irr  11686  exmidunben  11784  ssblex  12420  comet  12488  bdmopn  12493  divcnap  12541  cdivcncfap  12573  limcdifap  12587  limcimolemlt  12589  dvlemap  12604  dvidlemap  12615  dvcnp2cntop  12618  dvaddxxbr  12620  dvmulxxbr  12621  sbthom  12913  trilpo  12928