Theorem breq1 3985

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 3758	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	eleq1d 2235	. 2 |- ( A = B -> ( <. A , C >. e. R <-> <. B , C >. e. R ) )
3		df-br 3983	. 2 |- ( A R C <-> <. A , C >. e. R )
4		df-br 3983	. 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 1343   e. wcel 2136   <.cop 3579   class class class wbr 3982

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-br 3983

This theorem is referenced by:  breq12  3987  breq1i  3989  breq1d  3992  nbrne2  4002  brab1  4029  pocl  4281  swopolem  4283  swopo  4284  issod  4297  sowlin  4298  sotritrieq  4303  frirrg  4328  wetriext  4554  vtoclr  4652  brcog  4771  brcogw  4773  opelcnvg  4784  dfdmf  4797  eldmg  4799  dfrnf  4845  dfres2  4936  imasng  4969  coi1  5119  dffun6f  5201  funmo  5203  fun11  5255  fveq2  5486  funfveu  5499  sefvex  5507  nfunsn  5520  fvmptss2  5561  f1ompt  5636  fmptco  5651  dff13  5736  foeqcnvco  5758  isorel  5776  isocnv  5779  isotr  5784  isoini  5786  isopolem  5790  isosolem  5792  f1oiso  5794  f1oiso2  5795  caovordig  6007  caovordg  6009  caovord3d  6012  caovord  6013  caovord3  6015  caofrss  6074  caoftrn  6075  poxp  6200  brtpos2  6219  rntpos  6225  tpostpos  6232  ertr  6516  ecopovsym  6597  ecopovtrn  6598  ecopovsymg  6600  ecopovtrng  6601  th3qlem2  6604  isfi  6727  en0  6761  en1  6765  en1bg  6766  endisj  6790  xpcomco  6792  dom0  6804  ssenen  6817  nneneq  6823  domfiexmid  6844  findcard  6854  findcard2  6855  findcard2s  6856  isinfinf  6863  tridc  6865  fimax2gtrilemstep  6866  fimax2gtri  6867  fiintim  6894  fisseneq  6897  en1eqsnbi  6914  isbth  6932  supmoti  6958  eqsupti  6961  supubti  6964  suplubti  6965  supsnti  6970  isotilem  6971  isoti  6972  supisolem  6973  supisoex  6974  infminti  6992  isnumi  7138  cardval3ex  7141  oncardval  7142  cardonle  7143  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  nqtri3or  7337  ltsonq  7339  ltanqg  7341  ltmnqg  7342  ltexnqq  7349  subhalfnqq  7355  ltbtwnnqq  7356  archnqq  7358  nqnq0pi  7379  prcdnql  7425  prcunqu  7426  prnmaxl  7429  genpcuu  7461  genprndl  7462  genprndu  7463  nqprm  7483  nqprrnd  7484  nqprdisj  7485  nqprloc  7486  nqpru  7493  addnqprlemrl  7498  addnqprlemfl  7500  addnqprlemfu  7501  prmuloc2  7508  mulnqprlemrl  7514  mulnqprlemfl  7516  mulnqprlemfu  7517  1idprl  7531  ltnqpr  7534  ltnqpri  7535  prplnqu  7561  recexprlemell  7563  recexprlemm  7565  recexprlemdisj  7571  recexprlemloc  7572  recexprlem1ssu  7575  recexprlemss1l  7576  aptiprlemu  7581  archpr  7584  cauappcvgprlemm  7586  cauappcvgprlemladdfl  7596  cauappcvgprlem2  7601  cauappcvgpr  7603  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemcl  7617  caucvgprlem2  7621  caucvgpr  7623  caucvgprprlemelu  7627  caucvgprprlemcbv  7628  caucvgprprlemval  7629  caucvgprprlemnbj  7634  caucvgprprlemmu  7636  caucvgprprlemopu  7640  caucvgprprlemexbt  7647  caucvgprprlemaddq  7649  caucvgprprlem1  7650  caucvgprprlem2  7651  caucvgprpr  7653  suplocexprlemmu  7659  suplocexprlemloc  7662  suplocexpr  7666  lttrsr  7703  ltsosr  7705  1ne0sr  7707  ltasrg  7711  aptisr  7720  mulextsr1  7722  archsr  7723  caucvgsrlemgt1  7736  caucvgsrlemoffres  7741  caucvgsr  7743  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  axpre-ltwlin  7824  axpre-lttrn  7825  axpre-apti  7826  axpre-ltadd  7827  axpre-mulext  7829  axcaucvglemcau  7839  axcaucvglemres  7840  axcaucvg  7841  axpre-suploclemres  7842  axpre-suploc  7843  ltxrlt  7964  lttri3  7978  ltordlem  8380  lt0ne0d  8411  reapti  8477  apreim  8501  apsscn  8545  recexap  8550  lbreu  8840  lble  8842  suprleubex  8849  sup3exmid  8852  nnsub  8896  nominpos  9094  nn0n0n1ge2b  9270  zextle  9282  fzind  9306  btwnz  9310  uzval  9468  supinfneg  9533  infsupneg  9534  infregelbex  9536  ublbneg  9551  lbzbi  9554  qreccl  9580  xrltnsym  9729  xrlttr  9731  xrltso  9732  xrlttri3  9733  nltpnft  9750  npnflt  9751  xrrebnd  9755  xltnegi  9771  xnn0lenn0nn0  9801  xsubge0  9817  xlesubadd  9819  xleaddadd  9823  ixxval  9832  elixx1  9833  elioo2  9857  iccid  9861  fzval  9946  elfz1  9949  qtri3or  10178  exbtwnzlemstep  10183  exbtwnzlemshrink  10184  exbtwnzlemex  10185  exbtwnz  10186  rebtwn2zlemstep  10188  rebtwn2zlemshrink  10189  rebtwn2z  10190  qbtwnre  10192  qbtwnxr  10193  flval  10207  flqlelt  10211  flqbi  10225  flqeqceilz  10253  modqid2  10286  seq3f1olemqsum  10435  seq3f1oleml  10438  seq3f1o  10439  expcl2lemap  10467  expclzaplem  10479  expclzap  10480  expap0i  10487  nn0ltexp2  10623  hashinfuni  10690  hashennnuni  10692  hashunlem  10717  zfz1isolemiso  10752  zfz1isolem1  10753  zfz1iso  10754  absle  11031  maxleast  11155  rexanre  11162  rexico  11163  fimaxre2  11168  minmax  11171  xrmaxltsup  11199  xrminmax  11206  climshft  11245  reccn2ap  11254  summodclem3  11321  summodclem2a  11322  summodc  11324  zsumdc  11325  fsum3  11328  fsum3cvg3  11337  fsumcl2lem  11339  fsumadd  11347  sumsnf  11350  fsummulc2  11389  isumlessdc  11437  cvgratz  11473  mertenslemi1  11476  ntrivcvgap0  11490  prodmodclem3  11516  prodmodclem2a  11517  prodmodc  11519  zproddc  11520  fprodseq  11524  fprodntrivap  11525  fprodmul  11532  prodsnf  11533  absdvdsb  11749  zdvdsdc  11752  dvdsabseq  11785  dvdsdivcl  11788  dvdsext  11793  divalglemnn  11855  divalglemeunn  11858  divalglemeuneg  11860  divalgmod  11864  ndvdssub  11867  zsupcllemstep  11878  suprzubdc  11885  zsupssdc  11887  gcdsupex  11890  gcdsupcl  11891  gcddvds  11896  dvdslegcd  11897  bezoutlemmain  11931  bezoutlemex  11934  bezoutlemzz  11935  bezoutlemmo  11939  bezoutlemeu  11940  bezoutlemle  11941  bezoutlemsup  11942  dfgcd3  11943  dfgcd2  11947  gcdzeq  11955  dvdssq  11964  nnwodc  11969  uzwodc  11970  nnwofdc  11971  nn0seqcvgd  11973  algcvgblem  11981  lcmval  11995  lcmdvds  12011  lcmgcdeq  12015  coprmgcdb  12020  ncoprmgcdne1b  12021  coprmdvds1  12023  1nprm  12046  1idssfct  12047  isprm2lem  12048  isprm2  12049  dvdsprime  12054  nprm  12055  3prm  12060  dvdsprm  12069  exprmfct  12070  isprm5lem  12073  isprm5  12074  coprm  12076  sqrt2irr  12094  phisum  12172  odzval  12173  pythagtriplem4  12200  pc2dvds  12261  pcprmpw2  12264  pcprmpw  12265  dvdsprmpweqle  12268  oddprmdvds  12284  prmpwdvds  12285  pockthg  12287  1arith  12297  exmidunben  12359  nninfdclemcl  12381  nninfdclemp1  12383  nninfdc  12386  ssblex  13071  comet  13139  bdmopn  13144  reopnap  13178  divcnap  13195  cdivcncfap  13227  cnopnap  13234  dedekindeulemuub  13235  dedekindeulemloc  13237  dedekindeulemlu  13239  dedekindeulemeu  13240  dedekindeu  13241  suplociccreex  13242  dedekindicclemuub  13244  dedekindicclemloc  13246  dedekindicclemlu  13248  dedekindicclemeu  13249  dedekindicclemicc  13250  dedekindicc  13251  ivthinclemlopn  13254  ivthinclemlr  13255  ivthinclemuopn  13256  ivthinclemur  13257  ivthinclemloc  13259  ivthinc  13261  limcdifap  13271  limcimolemlt  13273  limccoap  13287  dvlemap  13289  dvidlemap  13300  dvcnp2cntop  13303  dvaddxxbr  13305  dvmulxxbr  13306  dvcoapbr  13311  dvcjbr  13312  dvrecap  13317  dveflem  13327  logltb  13435  2irrexpqap  13536  lgsmod  13567  lgsne0  13579  2sqlem6  13596  2sqlem8  13599  2sqlem10  13601  pw1nct  13883  sbthom  13905  trilpo  13922  trirec0  13923  reap0  13937  dcapnconst  13939  neapmkv  13946