Theorem breq1 4114

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 3885	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	eleq1d 2303	. 2 |- ( A = B -> ( <. A , C >. e. R <-> <. B , C >. e. R ) )
3		df-br 4112	. 2 |- ( A R C <-> <. A , C >. e. R )
4		df-br 4112	. 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 1398   e. wcel 2205   <.cop 3694   class class class wbr 4111

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-br 4112

This theorem is referenced by:  breq12  4116  breq1i  4118  breq1d  4121  nbrne2  4131  brab1  4159  pocl  4426  swopolem  4428  swopo  4429  issod  4442  sowlin  4443  sotritrieq  4448  frirrg  4473  wetriext  4701  vtoclr  4800  brcog  4924  brcogw  4926  opelcnvg  4937  dfdmf  4951  eldmg  4953  dfrnf  5000  dfres2  5092  imasng  5129  coi1  5280  dffun6f  5367  funmo  5369  fun11  5425  fveq2  5672  funfveu  5685  sefvex  5693  nfunsn  5709  fvmptss2  5754  f1ompt  5830  fmptco  5845  dff13  5943  foeqcnvco  5965  isorel  5983  isocnv  5986  isotr  5991  isoini  5993  isopolem  5997  isosolem  5999  f1oiso  6001  f1oiso2  6002  caovordig  6222  caovordg  6224  caovord3d  6227  caovord  6228  caovord3  6230  caofrss  6300  caoftrn  6301  poxp  6430  brtpos2  6484  rntpos  6490  tpostpos  6497  ertr  6784  ecopovsym  6867  ecopovtrn  6868  ecopovsymg  6870  ecopovtrng  6871  th3qlem2  6874  isfi  7002  en0  7037  en1  7041  en1bg  7042  endisj  7077  xpcomco  7079  dom0  7093  ssenen  7107  nneneq  7113  domfiexmid  7137  findcard  7147  findcard2  7148  findcard2s  7149  isinfinf  7156  tridc  7159  fimax2gtrilemstep  7160  fimax2gtri  7161  fiintim  7193  fisseneq  7197  en1eqsnbi  7221  isbth  7239  supmoti  7286  eqsupti  7289  supubti  7292  suplubti  7293  supsnti  7298  isotilem  7299  isoti  7300  supisolem  7301  supisoex  7302  infminti  7320  isnumi  7480  cardval3ex  7483  oncardval  7484  cardonle  7485  en2prde  7492  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  papsym  7563  papcotr  7564  exmidapne  7576  nqtri3or  7713  ltsonq  7715  ltanqg  7717  ltmnqg  7718  ltexnqq  7725  subhalfnqq  7731  ltbtwnnqq  7732  archnqq  7734  nqnq0pi  7755  prcdnql  7801  prcunqu  7802  prnmaxl  7805  genpcuu  7837  genprndl  7838  genprndu  7839  nqprm  7859  nqprrnd  7860  nqprdisj  7861  nqprloc  7862  nqpru  7869  addnqprlemrl  7874  addnqprlemfl  7876  addnqprlemfu  7877  prmuloc2  7884  mulnqprlemrl  7890  mulnqprlemfl  7892  mulnqprlemfu  7893  1idprl  7907  ltnqpr  7910  ltnqpri  7911  prplnqu  7937  recexprlemell  7939  recexprlemm  7941  recexprlemdisj  7947  recexprlemloc  7948  recexprlem1ssu  7951  recexprlemss1l  7952  aptiprlemu  7957  archpr  7960  cauappcvgprlemm  7962  cauappcvgprlemladdfl  7972  cauappcvgprlem2  7977  cauappcvgpr  7979  caucvgprlemnkj  7983  caucvgprlemnbj  7984  caucvgprlemcl  7993  caucvgprlem2  7997  caucvgpr  7999  caucvgprprlemelu  8003  caucvgprprlemcbv  8004  caucvgprprlemval  8005  caucvgprprlemnbj  8010  caucvgprprlemmu  8012  caucvgprprlemopu  8016  caucvgprprlemexbt  8023  caucvgprprlemaddq  8025  caucvgprprlem1  8026  caucvgprprlem2  8027  caucvgprpr  8029  suplocexprlemmu  8035  suplocexprlemloc  8038  suplocexpr  8042  lttrsr  8079  ltsosr  8081  1ne0sr  8083  ltasrg  8087  aptisr  8096  mulextsr1  8098  archsr  8099  caucvgsrlemgt1  8112  caucvgsrlemoffres  8117  caucvgsr  8119  suplocsrlemb  8123  suplocsrlempr  8124  suplocsrlem  8125  axpre-ltwlin  8200  axpre-lttrn  8201  axpre-apti  8202  axpre-ltadd  8203  axpre-mulext  8205  axcaucvglemcau  8215  axcaucvglemres  8216  axcaucvg  8217  axpre-suploclemres  8218  axpre-suploc  8219  ltxrlt  8341  lttri3  8355  ltordlem  8758  lt0ne0d  8789  reapti  8855  apreim  8879  apsscn  8923  recexap  8929  lbreu  9221  lble  9223  suprleubex  9230  sup3exmid  9233  nnsub  9278  nominpos  9478  nn0n0n1ge2b  9660  zextle  9672  fzind  9696  btwnz  9700  uzval  9858  supinfneg  9930  infsupneg  9931  infregelbex  9933  ublbneg  9948  lbzbi  9951  qreccl  9977  xrltnsym  10129  xrlttr  10131  xrltso  10132  xrlttri3  10133  nltpnft  10150  npnflt  10151  xrrebnd  10155  xltnegi  10171  xnn0lenn0nn0  10201  xsubge0  10217  xlesubadd  10219  xleaddadd  10223  ixxval  10232  elixx1  10233  elioo2  10257  iccid  10261  fzval  10347  elfz1  10350  zsupcllemstep  10593  suprzubdc  10600  zsupssdc  10602  qtri3or  10604  exbtwnzlemstep  10611  exbtwnzlemshrink  10612  exbtwnzlemex  10613  exbtwnz  10614  rebtwn2zlemstep  10616  rebtwn2zlemshrink  10617  rebtwn2z  10618  qbtwnre  10620  qbtwnxr  10621  flval  10636  flqlelt  10640  flqbi  10654  flqeqceilz  10684  modqid2  10717  seq3f1olemqsum  10879  seq3f1oleml  10882  seq3f1o  10883  seqf1oglem2  10886  expcl2lemap  10917  expclzaplem  10929  expclzap  10930  expap0i  10937  nn0ltexp2  11075  hashinfuni  11144  hashennnuni  11146  hashunlem  11172  zfz1isolemiso  11215  zfz1isolem1  11216  zfz1iso  11217  absle  11778  maxleast  11902  rexanre  11909  rexico  11910  fimaxre2  11916  minmax  11919  xrmaxltsup  11947  xrminmax  11954  climshft  11993  reccn2ap  12002  summodclem3  12070  summodclem2a  12071  summodc  12073  zsumdc  12074  fsum3  12077  fsum3cvg3  12086  fsumcl2lem  12088  fsumadd  12096  sumsnf  12099  fsummulc2  12138  isumlessdc  12186  cvgratz  12222  mertenslemi1  12225  ntrivcvgap0  12239  prodmodclem3  12265  prodmodclem2a  12266  prodmodc  12268  zproddc  12269  fprodseq  12273  fprodntrivap  12274  fprodmul  12281  prodsnf  12282  absdvdsb  12499  zdvdsdc  12502  dvdsabseq  12537  dvdsdivcl  12540  dvdsext  12545  divalglemnn  12608  divalglemeunn  12611  divalglemeuneg  12613  divalgmod  12617  ndvdssub  12620  gcdsupex  12657  gcdsupcl  12658  gcddvds  12663  dvdslegcd  12664  bezoutlemmain  12698  bezoutlemex  12701  bezoutlemzz  12702  bezoutlemmo  12706  bezoutlemeu  12707  bezoutlemle  12708  bezoutlemsup  12709  dfgcd3  12710  dfgcd2  12714  gcdzeq  12722  dvdssq  12731  nnwodc  12736  uzwodc  12737  nnwofdc  12738  nn0seqcvgd  12742  algcvgblem  12750  lcmval  12764  lcmdvds  12780  lcmgcdeq  12784  coprmgcdb  12789  ncoprmgcdne1b  12790  coprmdvds1  12792  1nprm  12815  1idssfct  12816  isprm2lem  12817  isprm2  12818  dvdsprime  12823  nprm  12824  3prm  12829  dvdsprm  12838  exprmfct  12839  isprm5lem  12842  isprm5  12843  coprm  12845  sqrt2irr  12863  dvdsfi  12940  phisum  12942  odzval  12943  pythagtriplem4  12970  pc2dvds  13032  pcprmpw2  13035  pcprmpw  13036  dvdsprmpweqle  13039  oddprmdvds  13056  prmpwdvds  13057  pockthg  13059  1arith  13069  ballotfilemfc0  13153  ballotfilemfcc  13154  exmidunben  13194  nninfdclemcl  13216  nninfdclemp1  13218  nninfdc  13221  imasaddfnlemg  13544  cnfldui  14754  znleval  14818  psrbagconcl  14844  ssblex  15313  comet  15381  bdmopn  15386  reopnap  15428  divcnap  15447  cdivcncfap  15486  cnopnap  15493  divcncfap  15496  maxcncf  15497  mincncf  15498  dedekindeulemuub  15499  dedekindeulemloc  15501  dedekindeulemlu  15503  dedekindeulemeu  15504  dedekindeu  15505  suplociccreex  15506  dedekindicclemuub  15508  dedekindicclemloc  15510  dedekindicclemlu  15512  dedekindicclemeu  15513  dedekindicclemicc  15514  dedekindicc  15515  ivthinclemlopn  15518  ivthinclemlr  15519  ivthinclemuopn  15520  ivthinclemur  15521  ivthinclemloc  15523  ivthinc  15525  ivthreinc  15527  dich0  15534  ivthdich  15535  limcdifap  15544  limcimolemlt  15546  limccoap  15560  dvlemap  15562  dvidlemap  15573  dvidrelem  15574  dvidsslem  15575  dvcnp2cntop  15581  dvaddxxbr  15583  dvmulxxbr  15584  dvcoapbr  15589  dvcjbr  15590  dvrecap  15595  dveflem  15608  logltb  15756  2irrexpqap  15860  sgmnncl  15873  dvdsppwf1o  15874  mpodvdsmulf1o  15875  perfectlem2  15885  lgsmod  15916  lgsne0  15928  gausslemma2dlem4  15954  2sqlem6  16010  2sqlem8  16013  2sqlem10  16015  upgrm  16112  upgr1or2  16113  umgredg2en  16121  umgrbien  16122  upgr1elem1  16132  umgr1een  16137  edgupgren  16153  edgumgren  16154  umgredgnlp  16164  edgusgren  16175  usgruspgrben  16198  usgr1e  16253  subumgredg2en  16283  subupgr  16285  wlkvtxiedg  16357  wlkvtxiedgg  16358  istrl  16397  iseupth  16459  eupth2fi  16491  konigsberglem1  16500  pw1nct  16794  sbthom  16823  trilpo  16844  trirec0  16845  reap0  16860  cndcap  16861  trimul0or  16862  dcapnconst  16864  neapmkv  16871  neap0mkv  16872  ltlenmkv  16873