Theorem breq1 3932

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 3705	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	eleq1d 2208	. 2 |- ( A = B -> ( <. A , C >. e. R <-> <. B , C >. e. R ) )
3		df-br 3930	. 2 |- ( A R C <-> <. A , C >. e. R )
4		df-br 3930	. 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 1331   e. wcel 1480   <.cop 3530   class class class wbr 3929

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930

This theorem is referenced by:  breq12  3934  breq1i  3936  breq1d  3939  nbrne2  3948  brab1  3975  pocl  4225  swopolem  4227  swopo  4228  issod  4241  sowlin  4242  sotritrieq  4247  frirrg  4272  wetriext  4491  vtoclr  4587  brcog  4706  brcogw  4708  opelcnvg  4719  dfdmf  4732  eldmg  4734  dfrnf  4780  dfres2  4871  imasng  4904  coi1  5054  dffun6f  5136  funmo  5138  fun11  5190  fveq2  5421  funfveu  5434  sefvex  5442  nfunsn  5455  fvmptss2  5496  f1ompt  5571  fmptco  5586  dff13  5669  foeqcnvco  5691  isorel  5709  isocnv  5712  isotr  5717  isoini  5719  isopolem  5723  isosolem  5725  f1oiso  5727  f1oiso2  5728  caovordig  5936  caovordg  5938  caovord3d  5941  caovord  5942  caovord3  5944  caofrss  6006  caoftrn  6007  poxp  6129  brtpos2  6148  rntpos  6154  tpostpos  6161  ertr  6444  ecopovsym  6525  ecopovtrn  6526  ecopovsymg  6528  ecopovtrng  6529  th3qlem2  6532  isfi  6655  en0  6689  en1  6693  en1bg  6694  endisj  6718  xpcomco  6720  dom0  6732  ssenen  6745  nneneq  6751  domfiexmid  6772  findcard  6782  findcard2  6783  findcard2s  6784  isinfinf  6791  tridc  6793  fimax2gtrilemstep  6794  fimax2gtri  6795  fiintim  6817  fisseneq  6820  en1eqsnbi  6837  isbth  6855  supmoti  6880  eqsupti  6883  supubti  6886  suplubti  6887  supsnti  6892  isotilem  6893  isoti  6894  supisolem  6895  supisoex  6896  infminti  6914  isnumi  7038  cardval3ex  7041  oncardval  7042  cardonle  7043  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  nqtri3or  7204  ltsonq  7206  ltanqg  7208  ltmnqg  7209  ltexnqq  7216  subhalfnqq  7222  ltbtwnnqq  7223  archnqq  7225  nqnq0pi  7246  prcdnql  7292  prcunqu  7293  prnmaxl  7296  genpcuu  7328  genprndl  7329  genprndu  7330  nqprm  7350  nqprrnd  7351  nqprdisj  7352  nqprloc  7353  nqpru  7360  addnqprlemrl  7365  addnqprlemfl  7367  addnqprlemfu  7368  prmuloc2  7375  mulnqprlemrl  7381  mulnqprlemfl  7383  mulnqprlemfu  7384  1idprl  7398  ltnqpr  7401  ltnqpri  7402  prplnqu  7428  recexprlemell  7430  recexprlemm  7432  recexprlemdisj  7438  recexprlemloc  7439  recexprlem1ssu  7442  recexprlemss1l  7443  aptiprlemu  7448  archpr  7451  cauappcvgprlemm  7453  cauappcvgprlemladdfl  7463  cauappcvgprlem2  7468  cauappcvgpr  7470  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemcl  7484  caucvgprlem2  7488  caucvgpr  7490  caucvgprprlemelu  7494  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemnbj  7501  caucvgprprlemmu  7503  caucvgprprlemopu  7507  caucvgprprlemexbt  7514  caucvgprprlemaddq  7516  caucvgprprlem1  7517  caucvgprprlem2  7518  caucvgprpr  7520  suplocexprlemmu  7526  suplocexprlemloc  7529  suplocexpr  7533  lttrsr  7570  ltsosr  7572  1ne0sr  7574  ltasrg  7578  aptisr  7587  mulextsr1  7589  archsr  7590  caucvgsrlemgt1  7603  caucvgsrlemoffres  7608  caucvgsr  7610  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  axpre-ltwlin  7691  axpre-lttrn  7692  axpre-apti  7693  axpre-ltadd  7694  axpre-mulext  7696  axcaucvglemcau  7706  axcaucvglemres  7707  axcaucvg  7708  axpre-suploclemres  7709  axpre-suploc  7710  ltxrlt  7830  lttri3  7844  ltordlem  8244  lt0ne0d  8275  reapti  8341  apreim  8365  apsscn  8409  recexap  8414  lbreu  8703  lble  8705  suprleubex  8712  sup3exmid  8715  nnsub  8759  nominpos  8957  nn0n0n1ge2b  9130  zextle  9142  fzind  9166  btwnz  9170  uzval  9328  supinfneg  9390  infsupneg  9391  ublbneg  9405  lbzbi  9408  qreccl  9434  xrltnsym  9579  xrlttr  9581  xrltso  9582  xrlttri3  9583  nltpnft  9597  npnflt  9598  xrrebnd  9602  xltnegi  9618  xnn0lenn0nn0  9648  xsubge0  9664  xlesubadd  9666  xleaddadd  9670  ixxval  9679  elixx1  9680  elioo2  9704  iccid  9708  fzval  9792  elfz1  9795  qtri3or  10020  exbtwnzlemstep  10025  exbtwnzlemshrink  10026  exbtwnzlemex  10027  exbtwnz  10028  rebtwn2zlemstep  10030  rebtwn2zlemshrink  10031  rebtwn2z  10032  qbtwnre  10034  qbtwnxr  10035  flval  10045  flqlelt  10049  flqbi  10063  flqeqceilz  10091  modqid2  10124  seq3f1olemqsum  10273  seq3f1oleml  10276  seq3f1o  10277  expcl2lemap  10305  expclzaplem  10317  expclzap  10318  expap0i  10325  hashinfuni  10523  hashennnuni  10525  hashunlem  10550  zfz1isolemiso  10582  zfz1isolem1  10583  zfz1iso  10584  absle  10861  maxleast  10985  rexanre  10992  rexico  10993  fimaxre2  10998  minmax  11001  xrmaxltsup  11027  xrminmax  11034  climshft  11073  reccn2ap  11082  summodclem3  11149  summodclem2a  11150  summodc  11152  zsumdc  11153  fsum3  11156  fsum3cvg3  11165  fsumcl2lem  11167  fsumadd  11175  sumsnf  11178  fsummulc2  11217  isumlessdc  11265  cvgratz  11301  mertenslemi1  11304  ntrivcvgap0  11318  prodmodclem3  11344  prodmodclem2a  11345  prodmodc  11347  absdvdsb  11511  zdvdsdc  11514  dvdsabseq  11545  dvdsdivcl  11548  dvdsext  11553  divalglemnn  11615  divalglemeunn  11618  divalglemeuneg  11620  divalgmod  11624  ndvdssub  11627  zsupcllemstep  11638  gcdsupex  11646  gcdsupcl  11647  gcddvds  11652  dvdslegcd  11653  bezoutlemmain  11686  bezoutlemex  11689  bezoutlemzz  11690  bezoutlemmo  11694  bezoutlemeu  11695  bezoutlemle  11696  bezoutlemsup  11697  dfgcd3  11698  dfgcd2  11702  gcdzeq  11710  dvdssq  11719  nn0seqcvgd  11722  algcvgblem  11730  lcmval  11744  lcmdvds  11760  lcmgcdeq  11764  coprmgcdb  11769  ncoprmgcdne1b  11770  coprmdvds1  11772  1nprm  11795  1idssfct  11796  isprm2lem  11797  isprm2  11798  dvdsprime  11803  nprm  11804  3prm  11809  dvdsprm  11817  exprmfct  11818  coprm  11822  sqrt2irr  11840  exmidunben  11939  ssblex  12600  comet  12668  bdmopn  12673  reopnap  12707  divcnap  12724  cdivcncfap  12756  cnopnap  12763  dedekindeulemuub  12764  dedekindeulemloc  12766  dedekindeulemlu  12768  dedekindeulemeu  12769  dedekindeu  12770  suplociccreex  12771  dedekindicclemuub  12773  dedekindicclemloc  12775  dedekindicclemlu  12777  dedekindicclemeu  12778  dedekindicclemicc  12779  dedekindicc  12780  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemloc  12788  ivthinc  12790  limcdifap  12800  limcimolemlt  12802  limccoap  12816  dvlemap  12818  dvidlemap  12829  dvcnp2cntop  12832  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  dvcjbr  12841  dvrecap  12846  dveflem  12855  sbthom  13221  trilpo  13236