Theorem breq1 4133

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 3904	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	eleq1d 2307	. 2 |- ( A = B -> ( <. A , C >. e. R <-> <. B , C >. e. R ) )
3		df-br 4131	. 2 |- ( A R C <-> <. A , C >. e. R )
4		df-br 4131	. 2 |- ( B R C <-> <. B , C >. e. R )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( A R C <-> B R C ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209   <.cop 3712   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  breq12  4135  breq1i  4137  breq1d  4140  nbrne2  4150  brab1  4178  pocl  4448  swopolem  4450  swopo  4451  issod  4464  sowlin  4465  sotritrieq  4470  frirrg  4495  wetriext  4724  vtoclr  4823  brcog  4947  brcogw  4949  opelcnvg  4960  dfdmf  4974  eldmg  4976  dfrnf  5023  dfres2  5115  imasng  5152  coi1  5303  dffun6f  5390  funmo  5392  fun11  5448  fveq2  5695  funfveu  5708  sefvex  5716  nfunsn  5733  fvmptss2  5780  f1ompt  5859  fmptco  5874  dff13  5974  foeqcnvco  5996  isorel  6014  isocnv  6017  isotr  6022  isoini  6024  isopolem  6028  isosolem  6030  f1oiso  6032  f1oiso2  6033  caovordig  6255  caovordg  6257  caovord3d  6260  caovord  6261  caovord3  6263  caofrss  6334  caoftrn  6335  poxp  6468  brtpos2  6522  rntpos  6528  tpostpos  6535  ertr  6822  ecopovsym  6905  ecopovtrn  6906  ecopovsymg  6908  ecopovtrng  6909  th3qlem2  6912  isfi  7047  en0  7082  en1  7086  en1bg  7087  endisj  7122  xpcomco  7124  dom0  7138  ssenen  7152  nneneq  7158  domfiexmid  7182  findcard  7192  findcard2  7193  findcard2s  7194  isinfinf  7201  tridc  7204  fimax2gtrilemstep  7205  fimax2gtri  7206  fiintim  7238  fisseneq  7242  en1eqsnbi  7266  isbth  7284  supmoti  7333  eqsupti  7336  supubti  7339  suplubti  7340  supsnti  7345  isotilem  7346  isoti  7347  supisolem  7348  supisoex  7349  infminti  7367  isnumi  7527  cardval3ex  7530  oncardval  7531  cardonle  7532  en2prde  7539  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  papsym  7612  papcotr  7613  exmidapne  7626  nqtri3or  7763  ltsonq  7765  ltanqg  7767  ltmnqg  7768  ltexnqq  7775  subhalfnqq  7781  ltbtwnnqq  7782  archnqq  7784  nqnq0pi  7805  prcdnql  7851  prcunqu  7852  prnmaxl  7855  genpcuu  7887  genprndl  7888  genprndu  7889  nqprm  7909  nqprrnd  7910  nqprdisj  7911  nqprloc  7912  nqpru  7919  addnqprlemrl  7924  addnqprlemfl  7926  addnqprlemfu  7927  prmuloc2  7934  mulnqprlemrl  7940  mulnqprlemfl  7942  mulnqprlemfu  7943  1idprl  7957  ltnqpr  7960  ltnqpri  7961  prplnqu  7987  recexprlemell  7989  recexprlemm  7991  recexprlemdisj  7997  recexprlemloc  7998  recexprlem1ssu  8001  recexprlemss1l  8002  aptiprlemu  8007  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemladdfl  8022  cauappcvgprlem2  8027  cauappcvgpr  8029  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemcl  8043  caucvgprlem2  8047  caucvgpr  8049  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnbj  8060  caucvgprprlemmu  8062  caucvgprprlemopu  8066  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgprpr  8079  suplocexprlemmu  8085  suplocexprlemloc  8088  suplocexpr  8092  lttrsr  8129  ltsosr  8131  1ne0sr  8133  ltasrg  8137  aptisr  8146  mulextsr1  8148  archsr  8149  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axpre-ltwlin  8250  axpre-lttrn  8251  axpre-apti  8252  axpre-ltadd  8253  axpre-mulext  8255  axcaucvglemcau  8265  axcaucvglemres  8266  axcaucvg  8267  axpre-suploclemres  8268  axpre-suploc  8269  ltxrlt  8391  lttri3  8405  ltordlem  8810  lt0ne0d  8841  reapti  8907  apreim  8931  apsscn  8975  recexap  8981  lbreu  9275  lble  9277  suprleubex  9284  sup3exmid  9287  nnsub  9343  nominpos  9543  nn0n0n1ge2b  9725  zextle  9737  fzind  9761  btwnz  9765  uzval  9923  supinfneg  9995  infsupneg  9996  infregelbex  9998  ublbneg  10013  lbzbi  10016  qreccl  10042  xrltnsym  10195  xrlttr  10197  xrltso  10198  xrlttri3  10199  nltpnft  10216  npnflt  10217  xrrebnd  10221  xltnegi  10237  xnn0lenn0nn0  10267  xsubge0  10283  xlesubadd  10285  xleaddadd  10289  ixxval  10298  elixx1  10299  elioo2  10323  iccid  10327  fzval  10413  elfz1  10416  zsupcllemstep  10662  suprzubdc  10671  zsupssdc  10673  qtri3or  10675  exbtwnzlemstep  10682  exbtwnzlemshrink  10683  exbtwnzlemex  10684  exbtwnz  10685  rebtwn2zlemstep  10687  rebtwn2zlemshrink  10688  rebtwn2z  10689  qbtwnre  10691  qbtwnxr  10692  flval  10707  flqlelt  10711  flqbi  10725  flqeqceilz  10755  modqid2  10788  seq3f1olemqsum  10950  seq3f1oleml  10953  seq3f1o  10954  seqf1oglem2  10957  expcl2lemap  10988  expclzaplem  11000  expclzap  11001  expap0i  11008  nn0ltexp2  11147  hashinfuni  11216  hashennnuni  11218  hashunlem  11244  zfz1isolemiso  11291  zfz1isolem1  11292  zfz1iso  11293  absle  11855  maxleast  11979  rexanre  11986  rexico  11987  fimaxre2  11993  minmax  11996  xrmaxltsup  12024  xrminmax  12031  climshft  12070  reccn2ap  12079  summodclem3  12147  summodclem2a  12148  summodc  12150  zsumdc  12151  fsum3  12154  fsum3cvg3  12163  fsumcl2lem  12165  fsumadd  12173  sumsnf  12176  fsummulc2  12215  isumlessdc  12263  cvgratz  12299  mertenslemi1  12302  ntrivcvgap0  12316  prodmodclem3  12342  prodmodclem2a  12343  prodmodc  12345  zproddc  12346  fprodseq  12350  fprodntrivap  12351  fprodmul  12358  prodsnf  12359  absdvdsb  12576  zdvdsdc  12579  dvdsabseq  12614  dvdsdivcl  12617  dvdsext  12622  divalglemnn  12685  divalglemeunn  12688  divalglemeuneg  12690  divalgmod  12694  ndvdssub  12697  gcdsupex  12734  gcdsupcl  12735  gcddvds  12740  dvdslegcd  12741  bezoutlemmain  12775  bezoutlemex  12778  bezoutlemzz  12779  bezoutlemmo  12783  bezoutlemeu  12784  bezoutlemle  12785  bezoutlemsup  12786  dfgcd3  12787  dfgcd2  12791  gcdzeq  12799  dvdssq  12808  nnwodc  12813  uzwodc  12814  nnwofdc  12815  nn0seqcvgd  12819  algcvgblem  12827  lcmval  12841  lcmdvds  12857  lcmgcdeq  12861  coprmgcdb  12866  ncoprmgcdne1b  12867  coprmdvds1  12869  1nprm  12892  1idssfct  12893  isprm2lem  12894  isprm2  12895  dvdsprime  12900  nprm  12901  3prm  12906  dvdsprm  12915  exprmfct  12916  isprm5lem  12919  isprm5  12920  coprm  12922  sqrt2irr  12940  dvdsfi  13017  phisum  13019  odzval  13020  pythagtriplem4  13047  pc2dvds  13109  pcprmpw2  13112  pcprmpw  13113  dvdsprmpweqle  13116  oddprmdvds  13133  prmpwdvds  13134  pockthg  13136  1arith  13146  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemsv  13253  ballotfilemsf1o  13257  ballotfi  13282  exmidunben  13317  nninfdclemcl  13339  nninfdclemp1  13341  nninfdc  13344  imasaddfnlemg  13635  ringunitsap0  14594  drnguiap  14609  cnfldui  14924  znleval  14988  psrbagconcl  15063  ssblex  15532  comet  15600  bdmopn  15605  reopnap  15647  divcnap  15666  cdivcncfap  15705  cnopnap  15712  divcncfap  15715  maxcncf  15716  mincncf  15717  dedekindeulemuub  15718  dedekindeulemloc  15720  dedekindeulemlu  15722  dedekindeulemeu  15723  dedekindeu  15724  suplociccreex  15725  dedekindicclemuub  15727  dedekindicclemloc  15729  dedekindicclemlu  15731  dedekindicclemeu  15732  dedekindicclemicc  15733  dedekindicc  15734  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemloc  15742  ivthinc  15744  ivthreinc  15746  dich0  15753  ivthdich  15754  limcdifap  15763  limcimolemlt  15765  limccoap  15779  dvlemap  15781  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  dvrecap  15814  dveflem  15827  logltb  15975  2irrexpqap  16080  sgmnncl  16102  dvdsppwf1o  16103  mpodvdsmulf1o  16104  perfectlem2  16114  lgsmod  16145  lgsne0  16157  gausslemma2dlem4  16183  2sqlem6  16239  2sqlem8  16242  2sqlem10  16244  upgrm  16341  upgr1or2  16342  umgredg2en  16350  umgrbien  16351  upgr1elem1  16361  umgr1een  16366  edgupgren  16382  edgumgren  16383  umgredgnlp  16393  edgusgren  16404  usgruspgrben  16427  usgr1e  16482  subumgredg2en  16512  subupgr  16514  wlkvtxiedg  16586  wlkvtxiedgg  16587  istrl  16626  iseupth  16688  eupth2fi  16720  konigsberglem1  16729  lealltlt1  16751  pw1nct  17033  sbthom  17071  trilpo  17092  trirec0  17093  reap0  17108  cndcap  17109  dcapnconst  17111  neapmkv  17118  neap0mkv  17119  ltlenmkv  17120