Theorem breq1 4004

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 3777	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	eleq1d 2246	. 2 |- ( A = B -> ( <. A , C >. e. R <-> <. B , C >. e. R ) )
3		df-br 4002	. 2 |- ( A R C <-> <. A , C >. e. R )
4		df-br 4002	. 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 1353   e. wcel 2148   <.cop 3595   class class class wbr 4001

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4002

This theorem is referenced by:  breq12  4006  breq1i  4008  breq1d  4011  nbrne2  4021  brab1  4048  pocl  4301  swopolem  4303  swopo  4304  issod  4317  sowlin  4318  sotritrieq  4323  frirrg  4348  wetriext  4574  vtoclr  4672  brcog  4791  brcogw  4793  opelcnvg  4804  dfdmf  4817  eldmg  4819  dfrnf  4865  dfres2  4956  imasng  4990  coi1  5141  dffun6f  5226  funmo  5228  fun11  5280  fveq2  5512  funfveu  5525  sefvex  5533  nfunsn  5546  fvmptss2  5588  f1ompt  5664  fmptco  5679  dff13  5764  foeqcnvco  5786  isorel  5804  isocnv  5807  isotr  5812  isoini  5814  isopolem  5818  isosolem  5820  f1oiso  5822  f1oiso2  5823  caovordig  6035  caovordg  6037  caovord3d  6040  caovord  6041  caovord3  6043  caofrss  6102  caoftrn  6103  poxp  6228  brtpos2  6247  rntpos  6253  tpostpos  6260  ertr  6545  ecopovsym  6626  ecopovtrn  6627  ecopovsymg  6629  ecopovtrng  6630  th3qlem2  6633  isfi  6756  en0  6790  en1  6794  en1bg  6795  endisj  6819  xpcomco  6821  dom0  6833  ssenen  6846  nneneq  6852  domfiexmid  6873  findcard  6883  findcard2  6884  findcard2s  6885  isinfinf  6892  tridc  6894  fimax2gtrilemstep  6895  fimax2gtri  6896  fiintim  6923  fisseneq  6926  en1eqsnbi  6943  isbth  6961  supmoti  6987  eqsupti  6990  supubti  6993  suplubti  6994  supsnti  6999  isotilem  7000  isoti  7001  supisolem  7002  supisoex  7003  infminti  7021  isnumi  7176  cardval3ex  7179  oncardval  7180  cardonle  7181  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  exmidapne  7254  nqtri3or  7390  ltsonq  7392  ltanqg  7394  ltmnqg  7395  ltexnqq  7402  subhalfnqq  7408  ltbtwnnqq  7409  archnqq  7411  nqnq0pi  7432  prcdnql  7478  prcunqu  7479  prnmaxl  7482  genpcuu  7514  genprndl  7515  genprndu  7516  nqprm  7536  nqprrnd  7537  nqprdisj  7538  nqprloc  7539  nqpru  7546  addnqprlemrl  7551  addnqprlemfl  7553  addnqprlemfu  7554  prmuloc2  7561  mulnqprlemrl  7567  mulnqprlemfl  7569  mulnqprlemfu  7570  1idprl  7584  ltnqpr  7587  ltnqpri  7588  prplnqu  7614  recexprlemell  7616  recexprlemm  7618  recexprlemdisj  7624  recexprlemloc  7625  recexprlem1ssu  7628  recexprlemss1l  7629  aptiprlemu  7634  archpr  7637  cauappcvgprlemm  7639  cauappcvgprlemladdfl  7649  cauappcvgprlem2  7654  cauappcvgpr  7656  caucvgprlemnkj  7660  caucvgprlemnbj  7661  caucvgprlemcl  7670  caucvgprlem2  7674  caucvgpr  7676  caucvgprprlemelu  7680  caucvgprprlemcbv  7681  caucvgprprlemval  7682  caucvgprprlemnbj  7687  caucvgprprlemmu  7689  caucvgprprlemopu  7693  caucvgprprlemexbt  7700  caucvgprprlemaddq  7702  caucvgprprlem1  7703  caucvgprprlem2  7704  caucvgprpr  7706  suplocexprlemmu  7712  suplocexprlemloc  7715  suplocexpr  7719  lttrsr  7756  ltsosr  7758  1ne0sr  7760  ltasrg  7764  aptisr  7773  mulextsr1  7775  archsr  7776  caucvgsrlemgt1  7789  caucvgsrlemoffres  7794  caucvgsr  7796  suplocsrlemb  7800  suplocsrlempr  7801  suplocsrlem  7802  axpre-ltwlin  7877  axpre-lttrn  7878  axpre-apti  7879  axpre-ltadd  7880  axpre-mulext  7882  axcaucvglemcau  7892  axcaucvglemres  7893  axcaucvg  7894  axpre-suploclemres  7895  axpre-suploc  7896  ltxrlt  8017  lttri3  8031  ltordlem  8433  lt0ne0d  8464  reapti  8530  apreim  8554  apsscn  8598  recexap  8604  lbreu  8896  lble  8898  suprleubex  8905  sup3exmid  8908  nnsub  8952  nominpos  9150  nn0n0n1ge2b  9326  zextle  9338  fzind  9362  btwnz  9366  uzval  9524  supinfneg  9589  infsupneg  9590  infregelbex  9592  ublbneg  9607  lbzbi  9610  qreccl  9636  xrltnsym  9787  xrlttr  9789  xrltso  9790  xrlttri3  9791  nltpnft  9808  npnflt  9809  xrrebnd  9813  xltnegi  9829  xnn0lenn0nn0  9859  xsubge0  9875  xlesubadd  9877  xleaddadd  9881  ixxval  9890  elixx1  9891  elioo2  9915  iccid  9919  fzval  10004  elfz1  10007  qtri3or  10236  exbtwnzlemstep  10241  exbtwnzlemshrink  10242  exbtwnzlemex  10243  exbtwnz  10244  rebtwn2zlemstep  10246  rebtwn2zlemshrink  10247  rebtwn2z  10248  qbtwnre  10250  qbtwnxr  10251  flval  10265  flqlelt  10269  flqbi  10283  flqeqceilz  10311  modqid2  10344  seq3f1olemqsum  10493  seq3f1oleml  10496  seq3f1o  10497  expcl2lemap  10525  expclzaplem  10537  expclzap  10538  expap0i  10545  nn0ltexp2  10681  hashinfuni  10748  hashennnuni  10750  hashunlem  10775  zfz1isolemiso  10810  zfz1isolem1  10811  zfz1iso  10812  absle  11089  maxleast  11213  rexanre  11220  rexico  11221  fimaxre2  11226  minmax  11229  xrmaxltsup  11257  xrminmax  11264  climshft  11303  reccn2ap  11312  summodclem3  11379  summodclem2a  11380  summodc  11382  zsumdc  11383  fsum3  11386  fsum3cvg3  11395  fsumcl2lem  11397  fsumadd  11405  sumsnf  11408  fsummulc2  11447  isumlessdc  11495  cvgratz  11531  mertenslemi1  11534  ntrivcvgap0  11548  prodmodclem3  11574  prodmodclem2a  11575  prodmodc  11577  zproddc  11578  fprodseq  11582  fprodntrivap  11583  fprodmul  11590  prodsnf  11591  absdvdsb  11807  zdvdsdc  11810  dvdsabseq  11843  dvdsdivcl  11846  dvdsext  11851  divalglemnn  11913  divalglemeunn  11916  divalglemeuneg  11918  divalgmod  11922  ndvdssub  11925  zsupcllemstep  11936  suprzubdc  11943  zsupssdc  11945  gcdsupex  11948  gcdsupcl  11949  gcddvds  11954  dvdslegcd  11955  bezoutlemmain  11989  bezoutlemex  11992  bezoutlemzz  11993  bezoutlemmo  11997  bezoutlemeu  11998  bezoutlemle  11999  bezoutlemsup  12000  dfgcd3  12001  dfgcd2  12005  gcdzeq  12013  dvdssq  12022  nnwodc  12027  uzwodc  12028  nnwofdc  12029  nn0seqcvgd  12031  algcvgblem  12039  lcmval  12053  lcmdvds  12069  lcmgcdeq  12073  coprmgcdb  12078  ncoprmgcdne1b  12079  coprmdvds1  12081  1nprm  12104  1idssfct  12105  isprm2lem  12106  isprm2  12107  dvdsprime  12112  nprm  12113  3prm  12118  dvdsprm  12127  exprmfct  12128  isprm5lem  12131  isprm5  12132  coprm  12134  sqrt2irr  12152  phisum  12230  odzval  12231  pythagtriplem4  12258  pc2dvds  12319  pcprmpw2  12322  pcprmpw  12323  dvdsprmpweqle  12326  oddprmdvds  12342  prmpwdvds  12343  pockthg  12345  1arith  12355  exmidunben  12417  nninfdclemcl  12439  nninfdclemp1  12441  nninfdc  12444  ssblex  13713  comet  13781  bdmopn  13786  reopnap  13820  divcnap  13837  cdivcncfap  13869  cnopnap  13876  dedekindeulemuub  13877  dedekindeulemloc  13879  dedekindeulemlu  13881  dedekindeulemeu  13882  dedekindeu  13883  suplociccreex  13884  dedekindicclemuub  13886  dedekindicclemloc  13888  dedekindicclemlu  13890  dedekindicclemeu  13891  dedekindicclemicc  13892  dedekindicc  13893  ivthinclemlopn  13896  ivthinclemlr  13897  ivthinclemuopn  13898  ivthinclemur  13899  ivthinclemloc  13901  ivthinc  13903  limcdifap  13913  limcimolemlt  13915  limccoap  13929  dvlemap  13931  dvidlemap  13942  dvcnp2cntop  13945  dvaddxxbr  13947  dvmulxxbr  13948  dvcoapbr  13953  dvcjbr  13954  dvrecap  13959  dveflem  13969  logltb  14077  2irrexpqap  14178  lgsmod  14209  lgsne0  14221  2sqlem6  14238  2sqlem8  14241  2sqlem10  14243  pw1nct  14523  sbthom  14545  trilpo  14562  trirec0  14563  reap0  14577  dcapnconst  14579  neapmkv  14586  neap0mkv  14587  ltlenmkv  14588