Theorem breq1 4032

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 3804	. . 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 4030	. 2 |- ( A R C <-> <. A , C >. e. R )
4		df-br 4030	. 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 3621   class class class wbr 4029

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 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030

This theorem is referenced by:  breq12  4034  breq1i  4036  breq1d  4039  nbrne2  4049  brab1  4076  pocl  4334  swopolem  4336  swopo  4337  issod  4350  sowlin  4351  sotritrieq  4356  frirrg  4381  wetriext  4609  vtoclr  4707  brcog  4829  brcogw  4831  opelcnvg  4842  dfdmf  4855  eldmg  4857  dfrnf  4903  dfres2  4994  imasng  5030  coi1  5181  dffun6f  5267  funmo  5269  fun11  5321  fveq2  5554  funfveu  5567  sefvex  5575  nfunsn  5589  fvmptss2  5632  f1ompt  5709  fmptco  5724  dff13  5811  foeqcnvco  5833  isorel  5851  isocnv  5854  isotr  5859  isoini  5861  isopolem  5865  isosolem  5867  f1oiso  5869  f1oiso2  5870  caovordig  6084  caovordg  6086  caovord3d  6089  caovord  6090  caovord3  6092  caofrss  6157  caoftrn  6158  poxp  6285  brtpos2  6304  rntpos  6310  tpostpos  6317  ertr  6602  ecopovsym  6685  ecopovtrn  6686  ecopovsymg  6688  ecopovtrng  6689  th3qlem2  6692  isfi  6815  en0  6849  en1  6853  en1bg  6854  endisj  6878  xpcomco  6880  dom0  6894  ssenen  6907  nneneq  6913  domfiexmid  6934  findcard  6944  findcard2  6945  findcard2s  6946  isinfinf  6953  tridc  6955  fimax2gtrilemstep  6956  fimax2gtri  6957  fiintim  6985  fisseneq  6988  en1eqsnbi  7008  isbth  7026  supmoti  7052  eqsupti  7055  supubti  7058  suplubti  7059  supsnti  7064  isotilem  7065  isoti  7066  supisolem  7067  supisoex  7068  infminti  7086  isnumi  7242  cardval3ex  7245  oncardval  7246  cardonle  7247  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidapne  7320  nqtri3or  7456  ltsonq  7458  ltanqg  7460  ltmnqg  7461  ltexnqq  7468  subhalfnqq  7474  ltbtwnnqq  7475  archnqq  7477  nqnq0pi  7498  prcdnql  7544  prcunqu  7545  prnmaxl  7548  genpcuu  7580  genprndl  7581  genprndu  7582  nqprm  7602  nqprrnd  7603  nqprdisj  7604  nqprloc  7605  nqpru  7612  addnqprlemrl  7617  addnqprlemfl  7619  addnqprlemfu  7620  prmuloc2  7627  mulnqprlemrl  7633  mulnqprlemfl  7635  mulnqprlemfu  7636  1idprl  7650  ltnqpr  7653  ltnqpri  7654  prplnqu  7680  recexprlemell  7682  recexprlemm  7684  recexprlemdisj  7690  recexprlemloc  7691  recexprlem1ssu  7694  recexprlemss1l  7695  aptiprlemu  7700  archpr  7703  cauappcvgprlemm  7705  cauappcvgprlemladdfl  7715  cauappcvgprlem2  7720  cauappcvgpr  7722  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemcl  7736  caucvgprlem2  7740  caucvgpr  7742  caucvgprprlemelu  7746  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemnbj  7753  caucvgprprlemmu  7755  caucvgprprlemopu  7759  caucvgprprlemexbt  7766  caucvgprprlemaddq  7768  caucvgprprlem1  7769  caucvgprprlem2  7770  caucvgprpr  7772  suplocexprlemmu  7778  suplocexprlemloc  7781  suplocexpr  7785  lttrsr  7822  ltsosr  7824  1ne0sr  7826  ltasrg  7830  aptisr  7839  mulextsr1  7841  archsr  7842  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  caucvgsr  7862  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  axpre-ltwlin  7943  axpre-lttrn  7944  axpre-apti  7945  axpre-ltadd  7946  axpre-mulext  7948  axcaucvglemcau  7958  axcaucvglemres  7959  axcaucvg  7960  axpre-suploclemres  7961  axpre-suploc  7962  ltxrlt  8085  lttri3  8099  ltordlem  8501  lt0ne0d  8532  reapti  8598  apreim  8622  apsscn  8666  recexap  8672  lbreu  8964  lble  8966  suprleubex  8973  sup3exmid  8976  nnsub  9021  nominpos  9220  nn0n0n1ge2b  9396  zextle  9408  fzind  9432  btwnz  9436  uzval  9594  supinfneg  9660  infsupneg  9661  infregelbex  9663  ublbneg  9678  lbzbi  9681  qreccl  9707  xrltnsym  9859  xrlttr  9861  xrltso  9862  xrlttri3  9863  nltpnft  9880  npnflt  9881  xrrebnd  9885  xltnegi  9901  xnn0lenn0nn0  9931  xsubge0  9947  xlesubadd  9949  xleaddadd  9953  ixxval  9962  elixx1  9963  elioo2  9987  iccid  9991  fzval  10076  elfz1  10079  qtri3or  10310  exbtwnzlemstep  10316  exbtwnzlemshrink  10317  exbtwnzlemex  10318  exbtwnz  10319  rebtwn2zlemstep  10321  rebtwn2zlemshrink  10322  rebtwn2z  10323  qbtwnre  10325  qbtwnxr  10326  flval  10341  flqlelt  10345  flqbi  10359  flqeqceilz  10389  modqid2  10422  seq3f1olemqsum  10584  seq3f1oleml  10587  seq3f1o  10588  seqf1oglem2  10591  expcl2lemap  10622  expclzaplem  10634  expclzap  10635  expap0i  10642  nn0ltexp2  10780  hashinfuni  10848  hashennnuni  10850  hashunlem  10875  zfz1isolemiso  10910  zfz1isolem1  10911  zfz1iso  10912  absle  11233  maxleast  11357  rexanre  11364  rexico  11365  fimaxre2  11370  minmax  11373  xrmaxltsup  11401  xrminmax  11408  climshft  11447  reccn2ap  11456  summodclem3  11523  summodclem2a  11524  summodc  11526  zsumdc  11527  fsum3  11530  fsum3cvg3  11539  fsumcl2lem  11541  fsumadd  11549  sumsnf  11552  fsummulc2  11591  isumlessdc  11639  cvgratz  11675  mertenslemi1  11678  ntrivcvgap0  11692  prodmodclem3  11718  prodmodclem2a  11719  prodmodc  11721  zproddc  11722  fprodseq  11726  fprodntrivap  11727  fprodmul  11734  prodsnf  11735  absdvdsb  11952  zdvdsdc  11955  dvdsabseq  11989  dvdsdivcl  11992  dvdsext  11997  divalglemnn  12059  divalglemeunn  12062  divalglemeuneg  12064  divalgmod  12068  ndvdssub  12071  zsupcllemstep  12082  suprzubdc  12089  zsupssdc  12091  gcdsupex  12094  gcdsupcl  12095  gcddvds  12100  dvdslegcd  12101  bezoutlemmain  12135  bezoutlemex  12138  bezoutlemzz  12139  bezoutlemmo  12143  bezoutlemeu  12144  bezoutlemle  12145  bezoutlemsup  12146  dfgcd3  12147  dfgcd2  12151  gcdzeq  12159  dvdssq  12168  nnwodc  12173  uzwodc  12174  nnwofdc  12175  nn0seqcvgd  12179  algcvgblem  12187  lcmval  12201  lcmdvds  12217  lcmgcdeq  12221  coprmgcdb  12226  ncoprmgcdne1b  12227  coprmdvds1  12229  1nprm  12252  1idssfct  12253  isprm2lem  12254  isprm2  12255  dvdsprime  12260  nprm  12261  3prm  12266  dvdsprm  12275  exprmfct  12276  isprm5lem  12279  isprm5  12280  coprm  12282  sqrt2irr  12300  phisum  12378  odzval  12379  pythagtriplem4  12406  pc2dvds  12468  pcprmpw2  12471  pcprmpw  12472  dvdsprmpweqle  12475  oddprmdvds  12492  prmpwdvds  12493  pockthg  12495  1arith  12505  exmidunben  12583  nninfdclemcl  12605  nninfdclemp1  12607  nninfdc  12610  imasaddfnlemg  12897  cnfldui  14077  znleval  14141  ssblex  14599  comet  14667  bdmopn  14672  reopnap  14706  divcnap  14723  cdivcncfap  14758  cnopnap  14765  divcncfap  14768  maxcncf  14769  mincncf  14770  dedekindeulemuub  14771  dedekindeulemloc  14773  dedekindeulemlu  14775  dedekindeulemeu  14776  dedekindeu  14777  suplociccreex  14778  dedekindicclemuub  14780  dedekindicclemloc  14782  dedekindicclemlu  14784  dedekindicclemeu  14785  dedekindicclemicc  14786  dedekindicc  14787  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemloc  14795  ivthinc  14797  ivthreinc  14799  dich0  14806  ivthdich  14807  limcdifap  14816  limcimolemlt  14818  limccoap  14832  dvlemap  14834  dvidlemap  14845  dvcnp2cntop  14848  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  dvrecap  14862  dveflem  14872  logltb  15009  2irrexpqap  15110  lgsmod  15142  lgsne0  15154  gausslemma2dlem4  15180  2sqlem6  15207  2sqlem8  15210  2sqlem10  15212  pw1nct  15493  sbthom  15516  trilpo  15533  trirec0  15534  reap0  15548  cndcap  15549  dcapnconst  15551  neapmkv  15558  neap0mkv  15559  ltlenmkv  15560