Theorem breq1 4134

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209   <.cop 3712   class class class wbr 4131

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4132

This theorem is used by:  breq12  4136  breq1i  4138  breq1d  4141  nbrne2  4151  brab1  4179  pocl  4450  swopolem  4452  swopo  4453  issod  4466  sowlin  4467  sotritrieq  4472  frirrg  4497  wetriext  4726  vtoclr  4825  brcog  4949  brcogw  4951  opelcnvg  4962  dfdmf  4976  eldmg  4978  dfrnf  5025  dfres2  5118  imasng  5155  coi1  5306  dffun6f  5393  funmo  5395  fun11  5451  fveq2  5698  funfveu  5711  sefvex  5719  nfunsn  5736  fvmptss2  5783  f1ompt  5862  fmptco  5877  dff13  5977  foeqcnvco  5999  isorel  6017  isocnv  6020  isotr  6025  isoini  6027  isopolem  6031  isosolem  6033  f1oiso  6035  f1oiso2  6036  caovordig  6258  caovordg  6260  caovord3d  6263  caovord  6264  caovord3  6266  caofrss  6338  caoftrn  6339  poxp  6472  brtpos2  6527  rntpos  6533  tpostpos  6540  ertr  6827  ecopovsym  6910  ecopovtrn  6911  ecopovsymg  6913  ecopovtrng  6914  th3qlem2  6917  isfi  7053  en0  7088  en1  7092  en1bg  7093  endisj  7128  xpcomco  7130  dom0  7144  ssenen  7158  nneneq  7164  domfiexmid  7188  findcard  7198  findcard2  7199  findcard2s  7200  isinfinf  7207  tridc  7210  fimax2gtrilemstep  7211  fimax2gtri  7212  fiintim  7244  fisseneq  7248  en1eqsnbi  7273  isbth  7291  supmoti  7339  eqsupti  7342  supubti  7345  suplubti  7346  supsnti  7351  isotilem  7352  isoti  7353  supisolem  7354  supisoex  7355  infminti  7373  isnumi  7533  cardval3ex  7536  oncardval  7537  cardonle  7538  en2prde  7545  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  papsym  7618  papcotr  7619  exmidapne  7632  nqtri3or  7769  ltsonq  7771  ltanqg  7773  ltmnqg  7774  ltexnqq  7781  subhalfnqq  7787  ltbtwnnqq  7788  archnqq  7790  nqnq0pi  7811  prcdnql  7857  prcunqu  7858  prnmaxl  7861  genpcuu  7893  genprndl  7894  genprndu  7895  nqprm  7915  nqprrnd  7916  nqprdisj  7917  nqprloc  7918  nqpru  7925  addnqprlemrl  7930  addnqprlemfl  7932  addnqprlemfu  7933  prmuloc2  7940  mulnqprlemrl  7946  mulnqprlemfl  7948  mulnqprlemfu  7949  1idprl  7963  ltnqpr  7966  ltnqpri  7967  prplnqu  7993  recexprlemell  7995  recexprlemm  7997  recexprlemdisj  8003  recexprlemloc  8004  recexprlem1ssu  8007  recexprlemss1l  8008  aptiprlemu  8013  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemladdfl  8028  cauappcvgprlem2  8033  cauappcvgpr  8035  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemcl  8049  caucvgprlem2  8053  caucvgpr  8055  caucvgprprlemelu  8059  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemnbj  8066  caucvgprprlemmu  8068  caucvgprprlemopu  8072  caucvgprprlemexbt  8079  caucvgprprlemaddq  8081  caucvgprprlem1  8082  caucvgprprlem2  8083  caucvgprpr  8085  suplocexprlemmu  8091  suplocexprlemloc  8094  suplocexpr  8098  lttrsr  8135  ltsosr  8137  1ne0sr  8139  ltasrg  8143  aptisr  8152  mulextsr1  8154  archsr  8155  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  caucvgsr  8175  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axpre-ltwlin  8256  axpre-lttrn  8257  axpre-apti  8258  axpre-ltadd  8259  axpre-mulext  8261  axcaucvglemcau  8271  axcaucvglemres  8272  axcaucvg  8273  axpre-suploclemres  8274  axpre-suploc  8275  ltxrlt  8397  lttri3  8411  ltordlem  8817  lt0ne0d  8848  reapti  8915  apreim  8939  apsscn  8983  recexap  8989  lbreu  9283  lble  9285  suprleubex  9292  sup3exmid  9295  nnsub  9352  nominpos  9554  nn0n0n1ge2b  9734  zextle  9747  fzind  9771  btwnz  9775  uzval  9938  supinfneg  10010  infsupneg  10011  infregelbex  10013  ublbneg  10028  lbzbi  10031  qreccl  10057  xrltnsym  10211  xrlttr  10213  xrltso  10214  xrlttri3  10215  nltpnft  10232  npnflt  10233  xrrebnd  10237  xltnegi  10253  xnn0lenn0nn0  10283  xsubge0  10299  xlesubadd  10301  xleaddadd  10305  ixxval  10314  elixx1  10315  elioo2  10339  iccid  10343  fzval  10429  elfz1  10432  zsupcllemstep  10678  suprzubdc  10687  zsupssdc  10689  qtri3or  10691  exbtwnzlemstep  10698  exbtwnzlemshrink  10699  exbtwnzlemex  10700  exbtwnz  10701  rebtwn2zlemstep  10703  rebtwn2zlemshrink  10704  rebtwn2z  10705  qbtwnre  10707  qbtwnxr  10708  flval  10723  flqlelt  10728  flaplelt  10729  flqbi  10745  flqeqceilz  10775  modqid2  10808  seq3f1olemqsum  10970  seq3f1oleml  10973  seq3f1o  10974  seqf1oglem2  10977  expcl2lemap  11008  expclzaplem  11020  expclzap  11021  expap0i  11028  nn0ltexp2  11168  hashinfuni  11237  hashennnuni  11239  hashunlem  11265  zfz1isolemiso  11312  zfz1isolem1  11313  zfz1iso  11314  absle  11877  maxleast  12001  rexanre  12008  rexico  12009  fimaxre2  12015  minmax  12019  xrmaxltsup  12048  xrminmax  12055  climshft  12094  reccn2ap  12103  summodclem3  12171  summodclem2a  12172  summodc  12174  zsumdc  12175  fsum3  12178  fsum3cvg3  12187  fsumcl2lem  12189  fsumadd  12197  sumsnf  12200  fsummulc2  12239  isumlessdc  12287  cvgratz  12323  mertenslemi1  12326  ntrivcvgap0  12340  prodmodclem3  12366  prodmodclem2a  12367  prodmodc  12369  zproddc  12370  fprodseq  12374  fprodntrivap  12375  fprodmul  12382  prodsnf  12383  absdvdsb  12600  zdvdsdc  12603  dvdsabseq  12638  dvdsdivcl  12641  dvdsext  12646  divalglemnn  12709  divalglemeunn  12712  divalglemeuneg  12714  divalgmod  12718  ndvdssub  12721  gcdsupex  12758  gcdsupcl  12759  gcddvds  12764  dvdslegcd  12765  bezoutlemmain  12799  bezoutlemex  12802  bezoutlemzz  12803  bezoutlemmo  12807  bezoutlemeu  12808  bezoutlemle  12809  bezoutlemsup  12810  dfgcd3  12811  dfgcd2  12815  gcdzeq  12823  dvdssq  12832  nnwodc  12837  uzwodc  12838  nnwofdc  12839  nn0seqcvgd  12843  algcvgblem  12851  lcmval  12865  lcmdvds  12881  lcmgcdeq  12885  coprmgcdb  12890  ncoprmgcdne1b  12891  coprmdvds1  12893  1nprm  12916  1idssfct  12917  isprm2lem  12918  isprm2  12919  dvdsprime  12924  nprm  12925  3prm  12930  dvdsprm  12940  exprmfct  12941  isprm5lem  12944  isprm5  12945  coprm  12947  sqrt2irr  12965  dvdsfi  13045  phisum  13047  odzval  13048  pythagtriplem4  13075  pc2dvds  13137  pcprmpw2  13140  pcprmpw  13141  dvdsprmpweqle  13144  oddprmdvds  13161  prmpwdvds  13162  pockthg  13164  1arith  13174  prmlem0  13248  prmlem1a  13249  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemsv  13310  ballotfilemsf1o  13314  ballotfi  13339  exmidunben  13374  nninfdclemcl  13396  nninfdclemp1  13398  nninfdc  13401  imasaddfnlemg  13693  ringunitsap0  14702  drnguiap  14717  cnfldui  15032  znleval  15096  psrbagconcl  15176  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  gsumbagdiaglem  15184  rhmpsrfilem2  15194  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  mplelbas  15224  ssblex  15674  comet  15742  bdmopn  15747  reopnap  15789  divcnap  15808  cdivcncfap  15847  cnopnap  15854  divcncfap  15857  maxcncf  15858  mincncf  15859  dedekindeulemuub  15860  dedekindeulemloc  15862  dedekindeulemlu  15864  dedekindeulemeu  15865  dedekindeu  15866  suplociccreex  15867  dedekindicclemuub  15869  dedekindicclemloc  15871  dedekindicclemlu  15873  dedekindicclemeu  15874  dedekindicclemicc  15875  dedekindicc  15876  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemloc  15884  ivthinc  15886  ivthreinc  15888  dich0  15895  ivthdich  15896  limcdifap  15905  limcimolemlt  15907  limccoap  15921  dvlemap  15923  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvrecap  15956  dveflem  15969  logltb  16121  2irrexpqap  16231  prmdvdsfi  16260  sgmnncl  16274  dvdsppwf1o  16300  mpodvdsmulf1o  16301  perfectlem2  16317  bcmono  16321  bpos1lem  16326  bposlem9  16336  lgsmod  16367  lgsne0  16379  gausslemma2dlem4  16405  2sqlem6  16461  2sqlem8  16464  2sqlem10  16466  upgrm  16563  upgr1or2  16564  umgredg2en  16572  umgrbien  16573  upgr1elem1  16583  umgr1een  16588  edgupgren  16604  edgumgren  16605  umgredgnlp  16615  edgusgren  16626  usgruspgrben  16649  usgr1e  16704  subumgredg2en  16734  subupgr  16736  wlkvtxiedg  16808  wlkvtxiedgg  16809  istrl  16848  iseupth  16910  eupth2fi  16942  konigsberglem1  16951  lealltlt1  16973  pw1nct  17255  sbthom  17294  rirrdisj  17308  trilpo  17316  trirec0  17317  reap0  17332  cndcap  17333  dcapnconst  17335  neapmkv  17342  neap0mkv  17343  ltlenmkv  17344