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

Theorem breq1 4028
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 3798 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2351 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 4026 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 4026 . 2  |-  ( B R C  <->  <. B ,  C >.  e.  R )
52, 3, 43bitr4g 279 1  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1625    e. wcel 1686   <.cop 3645   class class class wbr 4025
This theorem is referenced by:  breq12  4030  breq1i  4032  breq1d  4035  nbrne2  4043  brab1  4070  pocl  4323  swopolem  4325  swopo  4326  solin  4339  sotrieq  4343  sotr2  4345  isso2i  4348  somo  4350  frirr  4372  fr2nr  4373  wereu2  4392  fr3nr  4573  dfwe2  4575  vtoclr  4735  frsn  4762  brcog  4852  opelcnvg  4863  dfdmf  4875  eldmg  4876  dfrnf  4919  dfres2  5004  imasng  5037  asymref2  5062  sotri2  5074  somin1  5081  coi1  5190  dffun6f  5271  funmo  5273  fun11  5317  fveq2  5527  nfunsn  5560  dffv2  5594  dff3  5675  f1ompt  5684  fmptco  5693  dff13  5785  foeqcnvco  5806  isorel  5825  soisores  5826  soisoi  5827  isocnv  5829  isotr  5835  isomin  5836  isoini  5837  isopolem  5844  isosolem  5846  f1oiso  5850  f1oiso2  5851  f1oweALT  5853  weniso  5854  caovordig  6027  caovordg  6029  caovord3d  6032  caovord  6033  caovord3  6035  caofrss  6112  caoftrn  6114  frxp  6227  poxp  6229  fnse  6234  brtpos2  6242  rntpos  6249  tpostpos  6256  fvopab5  6291  ertr  6677  ecopovsym  6762  ecopovtrn  6763  th3qlem2  6767  isfi  6887  en0  6926  en1  6930  endisj  6951  xpcomco  6954  sbth  6983  2pwne  7019  disjenex  7021  ssenen  7037  nneneq  7046  php  7047  sdom1  7064  isinf  7078  fineqvlem  7079  pssnn  7083  enp1i  7095  findcard  7099  findcard2  7100  findcard3  7102  frfi  7104  fiint  7135  marypha1lem  7188  supmo  7205  eqsup  7209  supub  7212  suplub  7213  supmaxlem  7217  suppr  7221  supisolem  7223  supisoex  7224  ordtypecbv  7234  ordtypelem3  7237  ordtypelem6  7240  ordtypelem7  7241  ordtypelem9  7243  ordtypelem10  7244  hartogslem1  7259  hartogs  7261  wemaplem1  7263  wemaplem2  7264  card2on  7270  card2inf  7271  elharval  7279  brwdom2  7289  wdomtr  7291  cantnfp1lem2  7383  cantnflem1  7393  wemapwe  7402  r111  7449  kardex  7566  karden  7567  isnumi  7581  tskwe  7585  cardid2  7588  cardonle  7592  cardne  7600  iscard2  7611  infxpenlem  7643  fodomfi2  7689  wdomfil  7690  wdomnumr  7693  alephsuc2  7709  infenaleph  7720  iunfictbso  7743  infpss  7845  cff1  7886  cfslb2n  7896  sornom  7905  fin4i  7926  isfin6  7928  isfin7  7929  isfin1-3  8014  fin1a2lem9  8036  fin1a2lem11  8038  hsmexlem4  8057  axcc2lem  8064  axcc4dom  8069  domtriomlem  8070  numthcor  8123  zorn2lem2  8126  zorn2lem3  8127  zorn2lem7  8131  zorn2g  8132  axdclem  8148  axdc  8150  brdom7disj  8158  brdom6disj  8159  uniimadom  8168  ondomon  8187  alephval2  8196  alephreg  8206  pwcfsdom  8207  elgch  8246  gchi  8248  fpwwe2lem12  8265  fpwwe2lem13  8266  pwfseqlem4  8286  winainflem  8317  winalim2  8320  tsken  8378  0tsk  8379  inar1  8399  tskord  8404  tskuni  8407  grudomon  8441  pinq  8553  nqereu  8555  enqeq  8560  ltbtwnnq  8604  ltrnq  8605  prcdnq  8619  prnmax  8621  genpnmax  8633  nqpr  8640  1idpr  8655  reclem2pr  8674  reclem3pr  8675  reclem4pr  8676  recexpr  8677  supexpr  8680  ltsosr  8718  1ne0sr  8720  ltasr  8724  supsrlem  8735  axpre-lttri  8789  axpre-lttrn  8790  axpre-ltadd  8791  axpre-sup  8793  lelttr  8914  ltordlem  9300  lt0ne0d  9340  fimaxre3  9705  lbreu  9706  lble  9708  lbinfm  9709  sup2  9712  infm3  9715  suprleub  9720  supmul1  9721  supmullem1  9722  supmul  9724  nnsub  9786  nominpos  9950  nnunb  9963  arch  9964  nn0sub  10016  zextle  10087  peano5uzti  10103  fzind  10112  btwnz  10116  uzval  10234  uzwo  10283  uzwoOLD  10284  nnwof  10287  uzinfmi  10299  ublbneg  10304  lbzbi  10308  zsupss  10309  uzsupss  10312  uzwo3  10313  zmax  10315  rebtwnz  10317  rpnnen1lem3  10346  xrltnsym  10473  xrlttri  10475  xrlttr  10476  xrlelttr  10489  nltpnft  10497  xrmaxlt  10512  xrmaxle  10514  qbtwnre  10528  qbtwnxr  10529  xltnegi  10545  xsubge0  10583  xlesubadd  10585  xmullem2  10587  xlemul1a  10610  xrinfmexpnf  10626  xrsupsslem  10627  xrinfmsslem  10628  xrub  10632  supxrunb1  10640  supxrunb2  10641  ixxval  10666  elixx1  10667  elioo2  10699  iccid  10703  icc0  10706  fzval  10786  elfz1  10789  flval  10928  fllelt  10931  flval2  10946  flval3  10947  flbi  10948  modid2  10996  fsequb2  11040  seqf1olem2  11088  sqlecan  11211  faclbnd4lem1  11308  sqrlem6  11735  01sqrex  11737  abslt  11800  absle  11801  rexanre  11832  rexico  11839  limsupgle  11953  limsupgre  11957  limsupbnd2  11959  rlim2lt  11973  rlim3  11974  ello12r  11993  ello1d  11999  elo12r  12004  rlimconst  12020  climshft  12052  rlimcn2  12066  o1rlimmul  12094  lo1le  12127  climsup  12145  caucvgrlem  12147  isumless  12306  divrcnv  12313  cvgrat  12341  rpnnen2lem10  12504  ruclem1  12511  ruclem2  12512  ruclem11  12520  ruclem12  12521  sqr2irr  12529  absdvdsb  12549  dvdsle  12576  dvdseq  12578  dvdsext  12581  divalglem8  12601  divalglem9  12602  divalglem10  12603  divalgmod  12607  ndvdssub  12608  sadcaddlem  12650  gcdcllem1  12692  gcdcllem2  12693  gcdcllem3  12694  gcdeq  12733  dvdssq  12741  nn0seqcvgd  12742  algcvgblem  12749  1nprm  12765  1idssfct  12766  isprm2lem  12767  isprm2  12768  dvdsprime  12773  nprm  12774  3prm  12777  dvdsprm  12780  coprm  12781  exprmfct  12791  isprm5  12793  maxprmfct  12794  eulerthlem2  12852  odzval  12858  pythagtriplem4  12874  pc2dvds  12933  pcprmpw2  12936  pcprmpw  12937  prmpwdvds  12953  pockthg  12955  unbenlem  12957  prmreclem4  12968  prmreclem5  12969  prmreclem6  12970  1arith  12976  vdwlem6  13035  vdwlem11  13040  vdwlem13  13042  ramtlecl  13049  ramub  13062  rami  13064  ramubcl  13067  0ram  13069  ram0  13071  prmlem0  13109  prmlem1a  13110  imasaddfnlem  13432  imasvscafn  13441  imasleval  13445  prslem  14067  drsdir  14071  drsdirfi  14074  isdrs2  14075  posi  14086  posasymb  14088  pltval3  14103  plelttr  14108  pospo  14109  lubprop  14116  luble  14117  lubid  14118  glbprop  14121  joinval2  14125  joinlem  14126  meetlem  14133  meetle  14136  latnlej  14176  isglbd  14223  lubub  14225  lubun  14229  clatleglb  14232  pospropd  14240  poslubmo  14252  poslubd  14253  tsrlin  14330  spwmo  14337  spwpr2  14339  spwpr4  14342  letsr  14351  dirge  14361  mndodcongi  14860  odeq  14867  odmulgeq  14872  gexnnod  14901  sylow1lem1  14911  pgpssslw  14927  sylow2a  14932  efgredeu  15063  efgred2  15064  gexex  15147  frgpnabllem2  15164  cyggenod  15173  dprdval  15240  ablfacrplem  15302  ablfac1c  15308  ablfac1eu  15310  ablfaclem3  15324  abvtrivd  15607  psrbagconcl  16121  psrbagconf1o  16122  gsumbagdiaglem  16123  psrmulcllem  16134  psrlidm  16150  psrridm  16151  psrass1  16152  psrcom  16155  mplmonmul  16210  coe1mul2  16348  coe1tmmul  16355  zlpir  16446  prmirredlem  16448  znleval  16510  ordtbas2  16923  ordtopn2  16927  ordtrest2lem  16935  pnfnei  16952  ordtt1  17109  ordthauslem  17113  2ndci  17176  2ndcsb  17177  2ndcredom  17178  2ndc1stc  17179  1stcrest  17181  2ndcctbss  17183  2ndcdisj  17184  2ndcsep  17187  lly1stc  17224  tx1stc  17346  ordthmeolem  17494  ufildom1  17623  xmetrtri2  17922  prdsxmetlem  17934  ssblex  17976  prdsbl  18039  comet  18061  stdbdxmet  18063  stdbdmopn  18066  met1stc  18069  dscmet  18097  metdstri  18357  metdscn  18362  xrhmeo  18446  bndth  18458  evth  18459  lebnumlem3  18463  pcovalg  18512  pco1  18515  pcocn  18517  pcopt  18522  pcopt2  18523  pcoass  18524  nmoleub3  18602  bcthlem5  18752  minveclem4c  18791  minveclem2  18792  minveclem3b  18794  minveclem4  18798  minveclem6  18800  pmltpclem1  18810  pmltpc  18812  ovollb2lem  18849  ovolctb  18851  ovolunlem1  18858  ovoliunlem1  18863  ovoliunlem2  18864  ovoliun2  18867  ovolshftlem1  18870  ovolscalem1  18874  ovolicc1  18877  ovolicc2lem3  18880  voliunlem2  18910  voliunlem3  18911  ioombl1lem4  18920  uniioovol  18936  uniioombllem2  18940  uniioombllem3  18942  uniioombllem6  18945  volsup2  18962  ismbfd  18997  mbfsup  19021  mbflimsup  19023  itg1climres  19071  mbfi1fseqlem4  19075  itg2lr  19087  itg2leub  19091  itg2seq  19099  itg2monolem1  19107  itg2monolem3  19109  itg2mono  19110  itg2i1fseq2  19113  itg2gt0  19117  itg2cnlem1  19118  itg2cnlem2  19119  itg2cn  19120  iblss  19161  itgless  19173  ibladdlem  19176  iblabsr  19186  iblmulc2  19187  itgabs  19191  ditgeq1  19200  dvferm2lem  19335  rolle  19339  dvlip2  19344  c1liplem1  19345  c1lip1  19346  dvfsumlem2  19376  dvfsumlem4  19378  mdegleb  19452  degltlem1  19460  plyco0  19576  plyeq0lem  19594  coeeq2  19626  dgrle  19627  dgradd2  19651  plydiveu  19680  aareccl  19708  aalioulem2  19715  aaliou3lem7  19731  psercnlem1  19803  pilem2  19830  pilem3  19831  logltb  19955  divlogrlim  19984  logcnlem3  19993  cxpaddlelem  20093  rlimcnp  20262  cxplim  20268  cxploglim  20274  scvxcvx  20282  ftalem1  20312  ftalem2  20313  isppw2  20355  vmappw  20356  sgmnncl  20387  sqff1o  20422  dvdsdivcl  20423  fsumdvdsdiaglem  20425  dvdsppwf1o  20428  dvdsflsumcom  20430  musum  20433  muinv  20435  dvdsmulf1o  20436  vmalelog  20446  vmasum  20457  logfac2  20458  perfectlem2  20471  bcmono  20518  bpos1lem  20523  bposlem9  20533  lgsmod  20562  lgsne0  20574  2sqlem6  20610  2sqlem8  20613  2sqlem10  20615  chtppilim  20626  rpvmasumlem  20638  dchrisumlema  20639  dchrisumlem2  20641  dchrvmasumlem1  20646  dchrvmasumiflem1  20652  dchrisum0flblem1  20659  dchrisum0flblem2  20660  dchrisum0  20671  rplogsum  20678  logsqvma  20693  pntpbnd1  20737  pntpbnd2  20738  pntibndlem3  20743  pntlemj  20754  pntlemi  20755  pntlem3  20760  pnt3  20763  ostth3  20789  gxnval  20929  rngosn4  21096  rngoueqz  21099  nmoubi  21352  minvecolem2  21456  minvecolem3  21457  minvecolem4c  21460  minvecolem4  21461  minvecolem5  21462  minvecolem6  21463  htthlem  21499  chlimi  21816  chcompl  21824  hsn0elch  21829  cmbr3  22189  cmcm  22195  cmcm3  22196  lecm  22198  nmopub  22490  nmfnleub  22507  nmopun  22596  nmcexi  22608  cnlnadjlem7  22655  pjnmopi  22730  stle0i  22821  stlesi  22823  stm1i  22825  csmdsymi  22916  cvmd  22918  atcveq0  22930  atcv1  22962  atord  22970  atcvat2  22971  chirred  22977  mdsym  22994  mddmdin0i  23013  cdj1i  23015  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemsv  23070  ballotlemsf1o  23074  fmptcof2  23231  isoun  23244  lt2addrd  23251  xlt2addrd  23255  xrofsup  23257  xrge0iifiso  23319  xrge0addgt0  23333  rge0scvg  23375  esumpinfval  23443  esumpcvgval  23448  esumcvg  23456  sigaclcu  23480  sigaclci  23495  unelsiga  23497  measvun  23539  orvcval2  23661  dstfrvel  23676  eupath2  23906  relexpindlem  24038  rtrclreclem.trans  24045  dedekind  24084  dedekindle  24085  dfdm5  24134  dfrn5  24135  trpredpred  24233  poseq  24255  nodense  24345  nocvxminlem  24346  nobnddown  24357  nofulllem4  24361  nofulllem5  24362  brpprod  24427  brsset  24431  brbigcup  24440  dffix2  24447  elfuns  24456  brimageg  24468  brdomaing  24476  brrangeg  24477  brimg  24478  brapply  24479  brsuccf  24482  funpartfv  24485  brrestrict  24489  dfrdg4  24490  axlowdim2  24590  axlowdim  24591  axcontlem2  24595  axcontlem3  24596  axcontlem4  24597  axcontlem7  24600  axcontlem9  24602  axcontlem10  24603  axcontlem11  24604  axcontlem12  24605  brofs  24630  btwncomim  24638  btwnintr  24644  btwnexch3  24645  btwnexch2  24648  brifs  24668  brcolinear2  24683  colineardim1  24686  brfs  24704  btwnconn1  24726  segcon2  24730  seglerflx  24737  seglemin  24738  btwnsegle  24742  colinbtwnle  24743  broutsideof2  24747  fvray  24766  lineunray  24772  lineelsb2  24773  linerflx1  24774  supaddc  24927  supadd  24928  ltflcei  24930  lxflflp1  24932  itg2addnclem  24933  itg2addnc  24935  imgfldref2  25075  srefwref  25078  prj1b  25090  prj3  25091  oriso  25225  supdef  25273  supdefa  25274  ismxl2  25278  defse3  25283  inposet  25289  dfdir2  25302  cntrset  25613  supnuf  25640  fnctartar  25918  fnctartar2  25919  trer  26238  elicc3  26239  finminlem  26242  nn0prpwlem  26249  nn0prpw  26250  indexdom  26424  filbcmb  26443  fdc  26466  prdsbnd  26528  heiborlem3  26548  rrnequiv  26570  prtlem10  26744  lzenom  26860  fphpdo  26911  irrapxlem4  26921  pellexlem6  26930  infmrgelbi  26974  pellfundre  26977  pellfundlb  26980  monotoddzz  27039  zindbi  27042  divalgmodcl  27091  jm2.27  27112  rmydioph  27118  rpnnen3lem  27135  fnwe2lem2  27159  aomclem8  27170  hbtlem5  27343  hbt  27345  pmtrval  27405  pmtrrn  27410  pmtrfrn  27411  phisum  27529  rfcnnnub  27718  stoweidlem5  27765  stoweidlem7  27767  stoweidlem20  27780  stoweidlem26  27786  stoweidlem28  27788  stoweidlem29  27789  stoweidlem34  27794  wallispilem3  27827  stirlinglem13  27846  funressnfv  28002  dfdfat2  28005  tz6.12-afv  28046  usgra1v  28137  cusgra1v  28168  isfrgra  28182  3vfriswmgra  28194  1to2vfriswmgra  28195  sgnval  28256  bnj23  28817  bnj1185  28899  bnj1152  29101  bnj1418  29143  lubunNEW  29236  lsatcveq0  29295  lsatcv1  29311  oposlem  29446  opnlen0  29451  lub0N  29452  glb0N  29456  omllaw  29506  cmtbr4N  29518  cvrval  29532  cvrnbtwn  29534  cvrnbtwn2  29538  cvrnbtwn3  29539  cvrcon3b  29540  cvrnbtwn4  29542  atcvreq0  29577  atnle  29580  atlatmstc  29582  cvlexch1  29591  glbconN  29639  hlsuprexch  29643  exatleN  29666  cvratlem  29683  atcvrj0  29690  atcvrj2b  29694  atlelt  29700  cvrat4  29705  3dim1lem5  29728  3dim2  29730  3dim3  29731  ps-2  29740  llni  29770  llnn0  29778  llnle  29780  lplni  29794  lplni2  29799  lplnle  29802  lplnn0N  29809  llncvrlpln  29820  2llnjN  29829  lvoli  29837  lvoli3  29839  lvoli2  29843  lvoln0N  29853  4at  29875  lplncvrlvol  29878  2lplnj  29882  dalemcea  29922  dalem3  29926  psubspi  30009  linepsubN  30014  elpmap  30020  pmapsub  30030  lnatexN  30041  cdlema1N  30053  cdlemb  30056  elpadd  30061  paddvaln0N  30063  paddasslem5  30086  llnexchb2lem  30130  llnexch2N  30132  islhp  30258  lhpat3  30308  4atexlemex2  30333  4atex  30338  4atex2-0aOLDN  30340  4atex2-0cOLDN  30342  lautle  30346  lautcvr  30354  lauteq  30357  ldilval  30375  ltrnu  30383  trlval2  30425  trlne  30447  cdleme0ex1N  30485  cdleme0nex  30552  cdleme18d  30557  cdlemednuN  30562  cdleme25b  30616  cdleme25cv  30620  cdleme27b  30630  cdleme29b  30637  cdleme31sn  30642  cdleme31fv  30652  cdleme31fv2  30655  cdlemefrs29bpre0  30658  cdlemefr29bpre0N  30668  cdlemefr29clN  30669  cdlemefr32fvaN  30671  cdlemefr32fva1  30672  cdlemefs29pre00N  30674  cdlemefs32sn1aw  30676  cdlemefs29bpre0N  30678  cdlemefs29bpre1N  30679  cdlemefs29cpre1N  30680  cdlemefs29clN  30681  cdlemefs32fvaN  30684  cdlemefs32fva1  30685  cdleme41sn3a  30695  cdleme32fva  30699  cdleme32e  30707  cdleme35f  30716  cdleme40v  30731  cdleme42b  30740  trlord  30831  cdlemg1cex  30850  diaval  31295  diaeldm  31299  diaelrnN  31308  cdlemm10N  31381  dibglbN  31429  dicval  31439  dicfnN  31446  dicvalrelN  31448  dihval  31495  dihlsscpre  31497  dihglblem3N  31558  dihmeetlem2N  31562  djhcvat42  31678
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026
  Copyright terms: Public domain W3C validator