Theorem breq1 3992

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 3765	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	eleq1d 2239	. 2 |- ( A = B -> ( <. A , C >. e. R <-> <. B , C >. e. R ) )
3		df-br 3990	. 2 |- ( A R C <-> <. A , C >. e. R )
4		df-br 3990	. 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 1348   e. wcel 2141   <.cop 3586   class class class wbr 3989

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990

This theorem is referenced by:  breq12  3994  breq1i  3996  breq1d  3999  nbrne2  4009  brab1  4036  pocl  4288  swopolem  4290  swopo  4291  issod  4304  sowlin  4305  sotritrieq  4310  frirrg  4335  wetriext  4561  vtoclr  4659  brcog  4778  brcogw  4780  opelcnvg  4791  dfdmf  4804  eldmg  4806  dfrnf  4852  dfres2  4943  imasng  4976  coi1  5126  dffun6f  5211  funmo  5213  fun11  5265  fveq2  5496  funfveu  5509  sefvex  5517  nfunsn  5530  fvmptss2  5571  f1ompt  5647  fmptco  5662  dff13  5747  foeqcnvco  5769  isorel  5787  isocnv  5790  isotr  5795  isoini  5797  isopolem  5801  isosolem  5803  f1oiso  5805  f1oiso2  5806  caovordig  6018  caovordg  6020  caovord3d  6023  caovord  6024  caovord3  6026  caofrss  6085  caoftrn  6086  poxp  6211  brtpos2  6230  rntpos  6236  tpostpos  6243  ertr  6528  ecopovsym  6609  ecopovtrn  6610  ecopovsymg  6612  ecopovtrng  6613  th3qlem2  6616  isfi  6739  en0  6773  en1  6777  en1bg  6778  endisj  6802  xpcomco  6804  dom0  6816  ssenen  6829  nneneq  6835  domfiexmid  6856  findcard  6866  findcard2  6867  findcard2s  6868  isinfinf  6875  tridc  6877  fimax2gtrilemstep  6878  fimax2gtri  6879  fiintim  6906  fisseneq  6909  en1eqsnbi  6926  isbth  6944  supmoti  6970  eqsupti  6973  supubti  6976  suplubti  6977  supsnti  6982  isotilem  6983  isoti  6984  supisolem  6985  supisoex  6986  infminti  7004  isnumi  7159  cardval3ex  7162  oncardval  7163  cardonle  7164  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  nqtri3or  7358  ltsonq  7360  ltanqg  7362  ltmnqg  7363  ltexnqq  7370  subhalfnqq  7376  ltbtwnnqq  7377  archnqq  7379  nqnq0pi  7400  prcdnql  7446  prcunqu  7447  prnmaxl  7450  genpcuu  7482  genprndl  7483  genprndu  7484  nqprm  7504  nqprrnd  7505  nqprdisj  7506  nqprloc  7507  nqpru  7514  addnqprlemrl  7519  addnqprlemfl  7521  addnqprlemfu  7522  prmuloc2  7529  mulnqprlemrl  7535  mulnqprlemfl  7537  mulnqprlemfu  7538  1idprl  7552  ltnqpr  7555  ltnqpri  7556  prplnqu  7582  recexprlemell  7584  recexprlemm  7586  recexprlemdisj  7592  recexprlemloc  7593  recexprlem1ssu  7596  recexprlemss1l  7597  aptiprlemu  7602  archpr  7605  cauappcvgprlemm  7607  cauappcvgprlemladdfl  7617  cauappcvgprlem2  7622  cauappcvgpr  7624  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemcl  7638  caucvgprlem2  7642  caucvgpr  7644  caucvgprprlemelu  7648  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemnbj  7655  caucvgprprlemmu  7657  caucvgprprlemopu  7661  caucvgprprlemexbt  7668  caucvgprprlemaddq  7670  caucvgprprlem1  7671  caucvgprprlem2  7672  caucvgprpr  7674  suplocexprlemmu  7680  suplocexprlemloc  7683  suplocexpr  7687  lttrsr  7724  ltsosr  7726  1ne0sr  7728  ltasrg  7732  aptisr  7741  mulextsr1  7743  archsr  7744  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  caucvgsr  7764  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  axpre-ltwlin  7845  axpre-lttrn  7846  axpre-apti  7847  axpre-ltadd  7848  axpre-mulext  7850  axcaucvglemcau  7860  axcaucvglemres  7861  axcaucvg  7862  axpre-suploclemres  7863  axpre-suploc  7864  ltxrlt  7985  lttri3  7999  ltordlem  8401  lt0ne0d  8432  reapti  8498  apreim  8522  apsscn  8566  recexap  8571  lbreu  8861  lble  8863  suprleubex  8870  sup3exmid  8873  nnsub  8917  nominpos  9115  nn0n0n1ge2b  9291  zextle  9303  fzind  9327  btwnz  9331  uzval  9489  supinfneg  9554  infsupneg  9555  infregelbex  9557  ublbneg  9572  lbzbi  9575  qreccl  9601  xrltnsym  9750  xrlttr  9752  xrltso  9753  xrlttri3  9754  nltpnft  9771  npnflt  9772  xrrebnd  9776  xltnegi  9792  xnn0lenn0nn0  9822  xsubge0  9838  xlesubadd  9840  xleaddadd  9844  ixxval  9853  elixx1  9854  elioo2  9878  iccid  9882  fzval  9967  elfz1  9970  qtri3or  10199  exbtwnzlemstep  10204  exbtwnzlemshrink  10205  exbtwnzlemex  10206  exbtwnz  10207  rebtwn2zlemstep  10209  rebtwn2zlemshrink  10210  rebtwn2z  10211  qbtwnre  10213  qbtwnxr  10214  flval  10228  flqlelt  10232  flqbi  10246  flqeqceilz  10274  modqid2  10307  seq3f1olemqsum  10456  seq3f1oleml  10459  seq3f1o  10460  expcl2lemap  10488  expclzaplem  10500  expclzap  10501  expap0i  10508  nn0ltexp2  10644  hashinfuni  10711  hashennnuni  10713  hashunlem  10739  zfz1isolemiso  10774  zfz1isolem1  10775  zfz1iso  10776  absle  11053  maxleast  11177  rexanre  11184  rexico  11185  fimaxre2  11190  minmax  11193  xrmaxltsup  11221  xrminmax  11228  climshft  11267  reccn2ap  11276  summodclem3  11343  summodclem2a  11344  summodc  11346  zsumdc  11347  fsum3  11350  fsum3cvg3  11359  fsumcl2lem  11361  fsumadd  11369  sumsnf  11372  fsummulc2  11411  isumlessdc  11459  cvgratz  11495  mertenslemi1  11498  ntrivcvgap0  11512  prodmodclem3  11538  prodmodclem2a  11539  prodmodc  11541  zproddc  11542  fprodseq  11546  fprodntrivap  11547  fprodmul  11554  prodsnf  11555  absdvdsb  11771  zdvdsdc  11774  dvdsabseq  11807  dvdsdivcl  11810  dvdsext  11815  divalglemnn  11877  divalglemeunn  11880  divalglemeuneg  11882  divalgmod  11886  ndvdssub  11889  zsupcllemstep  11900  suprzubdc  11907  zsupssdc  11909  gcdsupex  11912  gcdsupcl  11913  gcddvds  11918  dvdslegcd  11919  bezoutlemmain  11953  bezoutlemex  11956  bezoutlemzz  11957  bezoutlemmo  11961  bezoutlemeu  11962  bezoutlemle  11963  bezoutlemsup  11964  dfgcd3  11965  dfgcd2  11969  gcdzeq  11977  dvdssq  11986  nnwodc  11991  uzwodc  11992  nnwofdc  11993  nn0seqcvgd  11995  algcvgblem  12003  lcmval  12017  lcmdvds  12033  lcmgcdeq  12037  coprmgcdb  12042  ncoprmgcdne1b  12043  coprmdvds1  12045  1nprm  12068  1idssfct  12069  isprm2lem  12070  isprm2  12071  dvdsprime  12076  nprm  12077  3prm  12082  dvdsprm  12091  exprmfct  12092  isprm5lem  12095  isprm5  12096  coprm  12098  sqrt2irr  12116  phisum  12194  odzval  12195  pythagtriplem4  12222  pc2dvds  12283  pcprmpw2  12286  pcprmpw  12287  dvdsprmpweqle  12290  oddprmdvds  12306  prmpwdvds  12307  pockthg  12309  1arith  12319  exmidunben  12381  nninfdclemcl  12403  nninfdclemp1  12405  nninfdc  12408  ssblex  13225  comet  13293  bdmopn  13298  reopnap  13332  divcnap  13349  cdivcncfap  13381  cnopnap  13388  dedekindeulemuub  13389  dedekindeulemloc  13391  dedekindeulemlu  13393  dedekindeulemeu  13394  dedekindeu  13395  suplociccreex  13396  dedekindicclemuub  13398  dedekindicclemloc  13400  dedekindicclemlu  13402  dedekindicclemeu  13403  dedekindicclemicc  13404  dedekindicc  13405  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemloc  13413  ivthinc  13415  limcdifap  13425  limcimolemlt  13427  limccoap  13441  dvlemap  13443  dvidlemap  13454  dvcnp2cntop  13457  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvrecap  13471  dveflem  13481  logltb  13589  2irrexpqap  13690  lgsmod  13721  lgsne0  13733  2sqlem6  13750  2sqlem8  13753  2sqlem10  13755  pw1nct  14036  sbthom  14058  trilpo  14075  trirec0  14076  reap0  14090  dcapnconst  14092  neapmkv  14099