Theorem breq1 4033

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 3805	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	eleq1d 2262	. 2 |- ( A = B -> ( <. A , C >. e. R <-> <. B , C >. e. R ) )
3		df-br 4031	. 2 |- ( A R C <-> <. A , C >. e. R )
4		df-br 4031	. 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 1364   e. wcel 2164   <.cop 3622   class class class wbr 4030

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031

This theorem is referenced by:  breq12  4035  breq1i  4037  breq1d  4040  nbrne2  4050  brab1  4077  pocl  4335  swopolem  4337  swopo  4338  issod  4351  sowlin  4352  sotritrieq  4357  frirrg  4382  wetriext  4610  vtoclr  4708  brcog  4830  brcogw  4832  opelcnvg  4843  dfdmf  4856  eldmg  4858  dfrnf  4904  dfres2  4995  imasng  5031  coi1  5182  dffun6f  5268  funmo  5270  fun11  5322  fveq2  5555  funfveu  5568  sefvex  5576  nfunsn  5590  fvmptss2  5633  f1ompt  5710  fmptco  5725  dff13  5812  foeqcnvco  5834  isorel  5852  isocnv  5855  isotr  5860  isoini  5862  isopolem  5866  isosolem  5868  f1oiso  5870  f1oiso2  5871  caovordig  6086  caovordg  6088  caovord3d  6091  caovord  6092  caovord3  6094  caofrss  6159  caoftrn  6160  poxp  6287  brtpos2  6306  rntpos  6312  tpostpos  6319  ertr  6604  ecopovsym  6687  ecopovtrn  6688  ecopovsymg  6690  ecopovtrng  6691  th3qlem2  6694  isfi  6817  en0  6851  en1  6855  en1bg  6856  endisj  6880  xpcomco  6882  dom0  6896  ssenen  6909  nneneq  6915  domfiexmid  6936  findcard  6946  findcard2  6947  findcard2s  6948  isinfinf  6955  tridc  6957  fimax2gtrilemstep  6958  fimax2gtri  6959  fiintim  6987  fisseneq  6990  en1eqsnbi  7010  isbth  7028  supmoti  7054  eqsupti  7057  supubti  7060  suplubti  7061  supsnti  7066  isotilem  7067  isoti  7068  supisolem  7069  supisoex  7070  infminti  7088  isnumi  7244  cardval3ex  7247  oncardval  7248  cardonle  7249  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidapne  7322  nqtri3or  7458  ltsonq  7460  ltanqg  7462  ltmnqg  7463  ltexnqq  7470  subhalfnqq  7476  ltbtwnnqq  7477  archnqq  7479  nqnq0pi  7500  prcdnql  7546  prcunqu  7547  prnmaxl  7550  genpcuu  7582  genprndl  7583  genprndu  7584  nqprm  7604  nqprrnd  7605  nqprdisj  7606  nqprloc  7607  nqpru  7614  addnqprlemrl  7619  addnqprlemfl  7621  addnqprlemfu  7622  prmuloc2  7629  mulnqprlemrl  7635  mulnqprlemfl  7637  mulnqprlemfu  7638  1idprl  7652  ltnqpr  7655  ltnqpri  7656  prplnqu  7682  recexprlemell  7684  recexprlemm  7686  recexprlemdisj  7692  recexprlemloc  7693  recexprlem1ssu  7696  recexprlemss1l  7697  aptiprlemu  7702  archpr  7705  cauappcvgprlemm  7707  cauappcvgprlemladdfl  7717  cauappcvgprlem2  7722  cauappcvgpr  7724  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemcl  7738  caucvgprlem2  7742  caucvgpr  7744  caucvgprprlemelu  7748  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemnbj  7755  caucvgprprlemmu  7757  caucvgprprlemopu  7761  caucvgprprlemexbt  7768  caucvgprprlemaddq  7770  caucvgprprlem1  7771  caucvgprprlem2  7772  caucvgprpr  7774  suplocexprlemmu  7780  suplocexprlemloc  7783  suplocexpr  7787  lttrsr  7824  ltsosr  7826  1ne0sr  7828  ltasrg  7832  aptisr  7841  mulextsr1  7843  archsr  7844  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  caucvgsr  7864  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  axpre-ltwlin  7945  axpre-lttrn  7946  axpre-apti  7947  axpre-ltadd  7948  axpre-mulext  7950  axcaucvglemcau  7960  axcaucvglemres  7961  axcaucvg  7962  axpre-suploclemres  7963  axpre-suploc  7964  ltxrlt  8087  lttri3  8101  ltordlem  8503  lt0ne0d  8534  reapti  8600  apreim  8624  apsscn  8668  recexap  8674  lbreu  8966  lble  8968  suprleubex  8975  sup3exmid  8978  nnsub  9023  nominpos  9223  nn0n0n1ge2b  9399  zextle  9411  fzind  9435  btwnz  9439  uzval  9597  supinfneg  9663  infsupneg  9664  infregelbex  9666  ublbneg  9681  lbzbi  9684  qreccl  9710  xrltnsym  9862  xrlttr  9864  xrltso  9865  xrlttri3  9866  nltpnft  9883  npnflt  9884  xrrebnd  9888  xltnegi  9904  xnn0lenn0nn0  9934  xsubge0  9950  xlesubadd  9952  xleaddadd  9956  ixxval  9965  elixx1  9966  elioo2  9990  iccid  9994  fzval  10079  elfz1  10082  qtri3or  10313  exbtwnzlemstep  10319  exbtwnzlemshrink  10320  exbtwnzlemex  10321  exbtwnz  10322  rebtwn2zlemstep  10324  rebtwn2zlemshrink  10325  rebtwn2z  10326  qbtwnre  10328  qbtwnxr  10329  flval  10344  flqlelt  10348  flqbi  10362  flqeqceilz  10392  modqid2  10425  seq3f1olemqsum  10587  seq3f1oleml  10590  seq3f1o  10591  seqf1oglem2  10594  expcl2lemap  10625  expclzaplem  10637  expclzap  10638  expap0i  10645  nn0ltexp2  10783  hashinfuni  10851  hashennnuni  10853  hashunlem  10878  zfz1isolemiso  10913  zfz1isolem1  10914  zfz1iso  10915  absle  11236  maxleast  11360  rexanre  11367  rexico  11368  fimaxre2  11373  minmax  11376  xrmaxltsup  11404  xrminmax  11411  climshft  11450  reccn2ap  11459  summodclem3  11526  summodclem2a  11527  summodc  11529  zsumdc  11530  fsum3  11533  fsum3cvg3  11542  fsumcl2lem  11544  fsumadd  11552  sumsnf  11555  fsummulc2  11594  isumlessdc  11642  cvgratz  11678  mertenslemi1  11681  ntrivcvgap0  11695  prodmodclem3  11721  prodmodclem2a  11722  prodmodc  11724  zproddc  11725  fprodseq  11729  fprodntrivap  11730  fprodmul  11737  prodsnf  11738  absdvdsb  11955  zdvdsdc  11958  dvdsabseq  11992  dvdsdivcl  11995  dvdsext  12000  divalglemnn  12062  divalglemeunn  12065  divalglemeuneg  12067  divalgmod  12071  ndvdssub  12074  zsupcllemstep  12085  suprzubdc  12092  zsupssdc  12094  gcdsupex  12097  gcdsupcl  12098  gcddvds  12103  dvdslegcd  12104  bezoutlemmain  12138  bezoutlemex  12141  bezoutlemzz  12142  bezoutlemmo  12146  bezoutlemeu  12147  bezoutlemle  12148  bezoutlemsup  12149  dfgcd3  12150  dfgcd2  12154  gcdzeq  12162  dvdssq  12171  nnwodc  12176  uzwodc  12177  nnwofdc  12178  nn0seqcvgd  12182  algcvgblem  12190  lcmval  12204  lcmdvds  12220  lcmgcdeq  12224  coprmgcdb  12229  ncoprmgcdne1b  12230  coprmdvds1  12232  1nprm  12255  1idssfct  12256  isprm2lem  12257  isprm2  12258  dvdsprime  12263  nprm  12264  3prm  12269  dvdsprm  12278  exprmfct  12279  isprm5lem  12282  isprm5  12283  coprm  12285  sqrt2irr  12303  phisum  12381  odzval  12382  pythagtriplem4  12409  pc2dvds  12471  pcprmpw2  12474  pcprmpw  12475  dvdsprmpweqle  12478  oddprmdvds  12495  prmpwdvds  12496  pockthg  12498  1arith  12508  exmidunben  12586  nninfdclemcl  12608  nninfdclemp1  12610  nninfdc  12613  imasaddfnlemg  12900  cnfldui  14088  znleval  14152  ssblex  14610  comet  14678  bdmopn  14683  reopnap  14725  divcnap  14744  cdivcncfap  14783  cnopnap  14790  divcncfap  14793  maxcncf  14794  mincncf  14795  dedekindeulemuub  14796  dedekindeulemloc  14798  dedekindeulemlu  14800  dedekindeulemeu  14801  dedekindeu  14802  suplociccreex  14803  dedekindicclemuub  14805  dedekindicclemloc  14807  dedekindicclemlu  14809  dedekindicclemeu  14810  dedekindicclemicc  14811  dedekindicc  14812  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemloc  14820  ivthinc  14822  ivthreinc  14824  dich0  14831  ivthdich  14832  limcdifap  14841  limcimolemlt  14843  limccoap  14857  dvlemap  14859  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvcnp2cntop  14878  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  dvrecap  14892  dveflem  14905  logltb  15050  2irrexpqap  15151  lgsmod  15183  lgsne0  15195  gausslemma2dlem4  15221  2sqlem6  15277  2sqlem8  15280  2sqlem10  15282  pw1nct  15563  sbthom  15586  trilpo  15603  trirec0  15604  reap0  15618  cndcap  15619  dcapnconst  15621  neapmkv  15628  neap0mkv  15629  ltlenmkv  15630