MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breq1 Unicode version

Theorem breq1 4149
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
StepHypRef Expression
1 opeq1 3919 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2446 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 4147 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 4147 . 2  |-  ( B R C  <->  <. B ,  C >.  e.  R )
52, 3, 43bitr4g 280 1  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1717   <.cop 3753   class class class wbr 4146
This theorem is referenced by:  breq12  4151  breq1i  4153  breq1d  4156  nbrne2  4164  brab1  4191  pocl  4444  swopolem  4446  swopo  4447  solin  4460  sotrieq  4464  sotr2  4466  isso2i  4469  somo  4471  frirr  4493  fr2nr  4494  wereu2  4513  fr3nr  4693  dfwe2  4695  vtoclr  4855  frsn  4881  brcog  4972  brcogw  4974  opelcnvg  4985  dfdmf  4997  eldmg  4998  dfrnf  5041  dfres2  5126  imasng  5159  asymref2  5184  sotri2  5196  somin1  5203  coi1  5318  dffun6f  5401  funmo  5403  fun11  5449  fveq2  5661  nfunsn  5694  dffv2  5728  dff3  5814  f1ompt  5823  fmptco  5833  dff13  5936  foeqcnvco  5959  isorel  5978  soisores  5979  soisoi  5980  isocnv  5982  isotr  5988  isomin  5989  isoini  5990  isopolem  5997  isosolem  5999  f1oiso  6003  f1oiso2  6004  f1oweALT  6006  weniso  6007  caovordig  6184  caovordg  6186  caovord3d  6189  caovord  6190  caovord3  6192  caofrss  6269  caoftrn  6271  frxp  6385  poxp  6387  fnse  6392  brtpos2  6414  rntpos  6421  tpostpos  6428  fvopab5  6463  ertr  6849  ecopovsym  6935  ecopovtrn  6936  th3qlem2  6940  isfi  7060  en0  7099  en1  7103  endisj  7124  xpcomco  7127  sbth  7156  2pwne  7192  disjenex  7194  ssenen  7210  nneneq  7219  php  7220  sdom1  7237  isinf  7251  fineqvlem  7252  pssnn  7256  enp1i  7272  findcard  7276  findcard2  7277  findcard3  7279  frfi  7281  fiint  7312  marypha1lem  7366  supmo  7383  eqsup  7387  supub  7390  suplub  7391  supmaxlem  7395  suppr  7399  supisolem  7401  supisoex  7402  ordtypecbv  7412  ordtypelem3  7415  ordtypelem6  7418  ordtypelem7  7419  ordtypelem9  7421  ordtypelem10  7422  hartogslem1  7437  hartogs  7439  wemaplem1  7441  wemaplem2  7442  card2on  7448  card2inf  7449  elharval  7457  brwdom2  7467  wdomtr  7469  cantnfp1lem2  7561  cantnflem1  7571  wemapwe  7580  r111  7627  kardex  7744  karden  7745  isnumi  7759  tskwe  7763  cardid2  7766  cardonle  7770  cardne  7778  iscard2  7789  infxpenlem  7821  fodomfi2  7867  wdomfil  7868  wdomnumr  7871  alephsuc2  7887  infenaleph  7898  iunfictbso  7921  infpss  8023  cff1  8064  cfslb2n  8074  sornom  8083  fin4i  8104  isfin6  8106  isfin7  8107  isfin1-3  8192  fin1a2lem9  8214  fin1a2lem11  8216  hsmexlem4  8235  axcc2lem  8242  axcc4dom  8247  domtriomlem  8248  numthcor  8300  zorn2lem2  8303  zorn2lem3  8304  zorn2lem7  8308  zorn2g  8309  axdclem  8325  axdc  8327  brdom7disj  8335  brdom6disj  8336  uniimadom  8345  ondomon  8364  alephval2  8373  alephreg  8383  pwcfsdom  8384  elgch  8423  gchi  8425  fpwwe2lem12  8442  fpwwe2lem13  8443  pwfseqlem4  8463  winainflem  8494  winalim2  8497  tsken  8555  0tsk  8556  inar1  8576  tskord  8581  tskuni  8584  grudomon  8618  pinq  8730  nqereu  8732  enqeq  8737  ltbtwnnq  8781  ltrnq  8782  prcdnq  8796  prnmax  8798  genpnmax  8810  nqpr  8817  1idpr  8832  reclem2pr  8851  reclem3pr  8852  reclem4pr  8853  recexpr  8854  supexpr  8857  ltsosr  8895  1ne0sr  8897  ltasr  8901  supsrlem  8912  axpre-lttri  8966  axpre-lttrn  8967  axpre-ltadd  8968  axpre-sup  8970  lelttr  9091  ltordlem  9477  lt0ne0d  9517  fimaxre3  9882  lbreu  9883  lble  9885  sup2  9889  infm3  9892  suprleub  9897  supmul1  9898  supmullem1  9899  supmul  9901  nnsub  9963  nominpos  10129  nnunb  10142  arch  10143  nn0sub  10195  nn0n0n1ge2b  10206  zextle  10268  peano5uzti  10284  fzind  10293  btwnz  10297  uzval  10415  uzwo  10464  uzwoOLD  10465  nnwof  10468  uzinfmi  10480  ublbneg  10485  lbzbi  10489  zsupss  10490  uzsupss  10493  uzwo3  10494  zmax  10496  rebtwnz  10498  rpnnen1lem3  10527  xrltnsym  10655  xrlttri  10657  xrlttr  10658  xrlelttr  10671  nltpnft  10679  xrmaxlt  10694  xrmaxle  10696  qbtwnre  10710  qbtwnxr  10711  xltnegi  10727  xsubge0  10765  xlesubadd  10767  xmullem2  10769  xlemul1a  10792  xrinfmexpnf  10809  xrsupsslem  10810  xrinfmsslem  10811  xrub  10815  supxrunb1  10823  supxrunb2  10824  ixxval  10849  elixx1  10850  elioo2  10882  iccid  10886  icc0  10889  fzval  10970  elfz1  10973  elfznelfzo  11112  elfznelfzob  11113  flval  11123  fllelt  11126  flval2  11141  flval3  11142  flbi  11143  modid2  11191  fsequb2  11235  seqf1olem2  11283  sqlecan  11407  faclbnd4lem1  11504  sqrlem6  11973  01sqrex  11975  abslt  12038  absle  12039  rexanre  12070  rexico  12077  limsupgle  12191  limsupgre  12195  limsupbnd2  12197  rlim2lt  12211  rlim3  12212  ello12r  12231  ello1d  12237  elo12r  12242  rlimconst  12258  climshft  12290  rlimcn2  12304  o1rlimmul  12332  lo1le  12365  climsup  12383  caucvgrlem  12386  isumless  12545  divrcnv  12552  cvgrat  12580  rpnnen2lem10  12743  ruclem1  12750  ruclem2  12751  ruclem11  12759  ruclem12  12760  sqr2irr  12768  absdvdsb  12788  dvdsle  12815  dvdseq  12817  dvdsext  12820  divalglem8  12840  divalglem9  12841  divalglem10  12842  divalgmod  12846  ndvdssub  12847  sadcaddlem  12889  gcdcllem1  12931  gcdcllem2  12932  gcdcllem3  12933  gcdeq  12972  dvdssq  12980  nn0seqcvgd  12981  algcvgblem  12988  1nprm  13004  1idssfct  13005  isprm2lem  13006  isprm2  13007  dvdsprime  13012  nprm  13013  3prm  13016  dvdsprm  13019  coprm  13020  exprmfct  13030  isprm5  13032  maxprmfct  13033  eulerthlem2  13091  odzval  13097  pythagtriplem4  13113  pc2dvds  13172  pcprmpw2  13175  pcprmpw  13176  prmpwdvds  13192  pockthg  13194  unbenlem  13196  prmreclem4  13207  prmreclem5  13208  prmreclem6  13209  1arith  13215  vdwlem6  13274  vdwlem11  13279  vdwlem13  13281  ramtlecl  13288  ramub  13301  rami  13303  ramubcl  13306  0ram  13308  ram0  13310  prmlem0  13348  prmlem1a  13349  imasaddfnlem  13673  imasvscafn  13682  imasleval  13686  prslem  14308  drsdir  14312  drsdirfi  14315  isdrs2  14316  posi  14327  posasymb  14329  pltval3  14344  plelttr  14349  pospo  14350  lubprop  14357  luble  14358  lubid  14359  glbprop  14362  joinval2  14366  joinlem  14367  meetlem  14374  meetle  14377  latnlej  14417  isglbd  14464  lubub  14466  lubun  14470  clatleglb  14473  pospropd  14481  poslubmo  14493  poslubd  14494  tsrlin  14571  spwmo  14578  spwpr2  14580  spwpr4  14583  letsr  14592  dirge  14602  mndodcongi  15101  odeq  15108  odmulgeq  15113  gexnnod  15142  sylow1lem1  15152  pgpssslw  15168  sylow2a  15173  efgredeu  15304  efgred2  15305  gexex  15388  frgpnabllem2  15405  cyggenod  15414  dprdval  15481  ablfacrplem  15543  ablfac1c  15549  ablfac1eu  15551  ablfaclem3  15565  abvtrivd  15848  psrbagconcl  16358  psrbagconf1o  16359  gsumbagdiaglem  16360  psrmulcllem  16371  psrlidm  16387  psrridm  16388  psrass1  16389  psrcom  16392  mplmonmul  16447  coe1mul2  16582  coe1tmmul  16589  zlpir  16687  prmirredlem  16689  znleval  16751  ordtbas2  17170  ordtopn2  17174  ordtrest2lem  17182  pnfnei  17199  ordtt1  17358  ordthauslem  17362  2ndci  17425  2ndcsb  17426  2ndcredom  17427  2ndc1stc  17428  1stcrest  17430  2ndcctbss  17432  2ndcdisj  17433  2ndcsep  17436  lly1stc  17473  tx1stc  17596  ordthmeolem  17747  ufildom1  17872  xmetrtri2  18287  prdsxmetlem  18299  ssblex  18341  prdsbl  18404  comet  18426  stdbdxmet  18428  stdbdmopn  18431  met1stc  18434  dscmet  18484  metdstri  18745  metdscn  18750  xrhmeo  18835  bndth  18847  evth  18848  lebnumlem3  18852  pcovalg  18901  pco1  18904  pcocn  18906  pcopt  18911  pcopt2  18912  pcoass  18913  nmoleub3  18991  bcthlem5  19143  minveclem4c  19186  minveclem2  19187  minveclem3b  19189  minveclem4  19193  minveclem6  19195  pmltpclem1  19205  pmltpc  19207  ovollb2lem  19244  ovolctb  19246  ovolunlem1  19253  ovoliunlem1  19258  ovoliunlem2  19259  ovoliun2  19262  ovolshftlem1  19265  ovolscalem1  19269  ovolicc1  19272  ovolicc2lem3  19275  voliunlem2  19305  voliunlem3  19306  ioombl1lem4  19315  uniioovol  19331  uniioombllem2  19335  uniioombllem3  19337  uniioombllem6  19340  volsup2  19357  ismbfd  19392  mbfsup  19416  mbflimsup  19418  itg1climres  19466  mbfi1fseqlem4  19470  itg2lr  19482  itg2leub  19486  itg2seq  19494  itg2monolem1  19502  itg2monolem3  19504  itg2mono  19505  itg2i1fseq2  19508  itg2gt0  19512  itg2cnlem1  19513  itg2cnlem2  19514  itg2cn  19515  iblss  19556  itgless  19568  ibladdlem  19571  iblabsr  19581  iblmulc2  19582  itgabs  19586  ditgeq1  19595  dvferm2lem  19730  rolle  19734  dvlip2  19739  c1liplem1  19740  c1lip1  19741  dvfsumlem2  19771  dvfsumlem4  19773  mdegleb  19847  degltlem1  19855  plyco0  19971  plyeq0lem  19989  coeeq2  20021  dgrle  20022  dgradd2  20046  plydiveu  20075  aareccl  20103  aalioulem2  20110  aaliou3lem7  20126  psercnlem1  20201  pilem2  20228  pilem3  20229  logltb  20354  divlogrlim  20386  logcnlem3  20395  cxpaddlelem  20495  rlimcnp  20664  cxplim  20670  cxploglim  20676  scvxcvx  20684  ftalem1  20715  ftalem2  20716  isppw2  20758  vmappw  20759  sgmnncl  20790  sqff1o  20825  dvdsdivcl  20826  fsumdvdsdiaglem  20828  dvdsppwf1o  20831  dvdsflsumcom  20833  musum  20836  muinv  20838  dvdsmulf1o  20839  vmalelog  20849  vmasum  20860  logfac2  20861  perfectlem2  20874  bcmono  20921  bpos1lem  20926  bposlem9  20936  lgsmod  20965  lgsne0  20977  2sqlem6  21013  2sqlem8  21016  2sqlem10  21018  chtppilim  21029  rpvmasumlem  21041  dchrisumlema  21042  dchrisumlem2  21044  dchrvmasumlem1  21049  dchrvmasumiflem1  21055  dchrisum0flblem1  21062  dchrisum0flblem2  21063  dchrisum0  21074  rplogsum  21081  logsqvma  21096  pntpbnd1  21140  pntpbnd2  21141  pntibndlem3  21146  pntlemj  21157  pntlemi  21158  pntlem3  21163  pnt3  21166  ostth3  21192  usisuslgra  21247  usgra1v  21268  usgrafisindb0  21281  usgrafisindb1  21282  cusgra1v  21329  1conngra  21503  eupath2  21543  gxnval  21689  rngosn4  21856  rngoueqz  21859  nmoubi  22114  minvecolem2  22218  minvecolem3  22219  minvecolem4c  22222  minvecolem4  22223  minvecolem5  22224  minvecolem6  22225  htthlem  22261  chlimi  22578  chcompl  22586  hsn0elch  22591  cmbr3  22951  cmcm  22957  cmcm3  22958  lecm  22960  nmopub  23252  nmfnleub  23269  nmopun  23358  nmcexi  23370  cnlnadjlem7  23417  pjnmopi  23492  stle0i  23583  stlesi  23585  stm1i  23587  csmdsymi  23678  cvmd  23680  atcveq0  23692  atcv1  23724  atord  23732  atcvat2  23733  chirred  23739  mdsym  23756  mddmdin0i  23775  cdj1i  23777  fmptcof2  23911  isoun  23923  lt2addrd  23949  xlt2addrd  23953  xrofsup  23955  ofldadd  24057  ofldmul  24058  xrge0iifiso  24118  rge0scvg  24132  gsumesum  24240  esumfsup  24249  esumpinfval  24252  esumpcvgval  24257  esumcvg  24265  sigaclcu  24289  sigaclci  24304  unelsiga  24306  measvun  24350  voliune  24372  volfiniune  24373  orvcval2  24488  dstfrvel  24503  ballotlemfc0  24522  ballotlemfcc  24523  ballotlemsv  24539  ballotlemsf1o  24543  relexpindlem  24911  rtrclreclem.trans  24918  dedekind  24959  dedekindle  24960  dfdm5  25149  dfrn5  25150  trpredpred  25248  poseq  25270  nodense  25360  nocvxminlem  25361  nobnddown  25372  nofulllem4  25376  nofulllem5  25377  brpprod  25442  brsset  25446  brbigcup  25455  dffix2  25462  elfuns  25471  brimageg  25483  brdomaing  25491  brrangeg  25492  brimg  25493  brapply  25494  brsuccf  25497  funpartlem  25498  brrestrict  25505  dfrdg4  25506  axlowdim2  25606  axlowdim  25607  axcontlem2  25611  axcontlem3  25612  axcontlem4  25613  axcontlem7  25616  axcontlem9  25618  axcontlem10  25619  axcontlem11  25620  axcontlem12  25621  brofs  25646  btwncomim  25654  btwnintr  25660  btwnexch3  25661  btwnexch2  25664  brifs  25684  brcolinear2  25699  colineardim1  25702  brfs  25720  btwnconn1  25742  segcon2  25746  seglerflx  25753  seglemin  25754  btwnsegle  25758  colinbtwnle  25759  broutsideof2  25763  fvray  25782  lineunray  25788  lineelsb2  25789  linerflx1  25790  supaddc  25940  supadd  25941  ltflcei  25943  lxflflp1  25945  itg2addnclem  25950  itg2addnc  25952  itg2gt0cn  25953  ibladdnclem  25954  iblmulc2nc  25963  itgabsnc  25967  bddiblnc  25968  trer  26003  elicc3  26004  finminlem  26005  nn0prpwlem  26009  nn0prpw  26010  indexdom  26120  filbcmb  26126  fdc  26133  prdsbnd  26186  heiborlem3  26206  rrnequiv  26228  prtlem10  26398  lzenom  26512  fphpdo  26562  irrapxlem4  26572  pellexlem6  26581  infmrgelbi  26625  pellfundre  26628  pellfundlb  26631  monotoddzz  26690  zindbi  26693  divalgmodcl  26742  jm2.27  26763  rmydioph  26769  rpnnen3lem  26786  fnwe2lem2  26810  aomclem8  26821  hbtlem5  26994  hbt  26996  pmtrval  27056  pmtrrn  27061  pmtrfrn  27062  phisum  27180  stoweidlem5  27415  stoweidlem20  27430  stoweidlem26  27436  stoweidlem28  27438  stoweidlem29  27439  stoweidlem34  27444  wallispilem3  27477  stirlinglem13  27496  funressnfv  27654  dfdfat2  27657  tz6.12-afv  27699  isfrgra  27736  3vfriswmgra  27751  1to2vfriswmgra  27752  vdfrgra0  27768  vdgfrgra0  27769  sgnval  27857  bnj23  28414  bnj1185  28496  bnj1152  28698  bnj1418  28740  lubunNEW  29139  lsatcveq0  29198  lsatcv1  29214  oposlem  29349  opnlen0  29354  lub0N  29355  glb0N  29359  omllaw  29409  cmtbr4N  29421  cvrval  29435  cvrnbtwn  29437  cvrnbtwn2  29441  cvrnbtwn3  29442  cvrcon3b  29443  cvrnbtwn4  29445  atcvreq0  29480  atnle  29483  atlatmstc  29485  cvlexch1  29494  glbconN  29542  hlsuprexch  29546  exatleN  29569  cvratlem  29586  atcvrj0  29593  atcvrj2b  29597  atlelt  29603  cvrat4  29608  3dim1lem5  29631  3dim2  29633  3dim3  29634  ps-2  29643  llni  29673  llnn0  29681  llnle  29683  lplni  29697  lplni2  29702  lplnle  29705  lplnn0N  29712  llncvrlpln  29723  2llnjN  29732  lvoli  29740  lvoli3  29742  lvoli2  29746  lvoln0N  29756  4at  29778  lplncvrlvol  29781  2lplnj  29785  dalemcea  29825  dalem3  29829  psubspi  29912  linepsubN  29917  elpmap  29923  pmapsub  29933  lnatexN  29944  cdlema1N  29956  cdlemb  29959  elpadd  29964  paddvaln0N  29966  paddasslem5  29989  llnexchb2lem  30033  llnexch2N  30035  islhp  30161  lhpat3  30211  4atexlemex2  30236  4atex  30241  4atex2-0aOLDN  30243  4atex2-0cOLDN  30245  lautle  30249  lautcvr  30257  lauteq  30260  ldilval  30278  ltrnu  30286  trlval2  30328  trlne  30350  cdleme0ex1N  30388  cdleme0nex  30455  cdleme18d  30460  cdlemednuN  30465  cdleme25b  30519  cdleme25cv  30523  cdleme27b  30533  cdleme29b  30540  cdleme31sn  30545  cdleme31fv  30555  cdleme31fv2  30558  cdlemefrs29bpre0  30561  cdlemefr29bpre0N  30571  cdlemefr29clN  30572  cdlemefr32fvaN  30574  cdlemefr32fva1  30575  cdlemefs29pre00N  30577  cdlemefs32sn1aw  30579  cdlemefs29bpre0N  30581  cdlemefs29bpre1N  30582  cdlemefs29cpre1N  30583  cdlemefs29clN  30584  cdlemefs32fvaN  30587  cdlemefs32fva1  30588  cdleme41sn3a  30598  cdleme32fva  30602  cdleme32e  30610  cdleme35f  30619  cdleme40v  30634  cdleme42b  30643  trlord  30734  cdlemg1cex  30753  diaval  31198  diaeldm  31202  diaelrnN  31211  cdlemm10N  31284  dibglbN  31332  dicval  31342  dicfnN  31349  dicvalrelN  31351  dihval  31398  dihlsscpre  31400  dihglblem3N  31461  dihmeetlem2N  31465  djhcvat42  31581
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-br 4147
  Copyright terms: Public domain W3C validator