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

Theorem breq1 4042
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 3812 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2362 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 4040 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 4040 . 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 1632    e. wcel 1696   <.cop 3656   class class class wbr 4039
This theorem is referenced by:  breq12  4044  breq1i  4046  breq1d  4049  nbrne2  4057  brab1  4084  pocl  4337  swopolem  4339  swopo  4340  solin  4353  sotrieq  4357  sotr2  4359  isso2i  4362  somo  4364  frirr  4386  fr2nr  4387  wereu2  4406  fr3nr  4587  dfwe2  4589  vtoclr  4749  frsn  4776  brcog  4866  opelcnvg  4877  dfdmf  4889  eldmg  4890  dfrnf  4933  dfres2  5018  imasng  5051  asymref2  5076  sotri2  5088  somin1  5095  coi1  5204  dffun6f  5285  funmo  5287  fun11  5331  fveq2  5541  nfunsn  5574  dffv2  5608  dff3  5689  f1ompt  5698  fmptco  5707  dff13  5799  foeqcnvco  5820  isorel  5839  soisores  5840  soisoi  5841  isocnv  5843  isotr  5849  isomin  5850  isoini  5851  isopolem  5858  isosolem  5860  f1oiso  5864  f1oiso2  5865  f1oweALT  5867  weniso  5868  caovordig  6041  caovordg  6043  caovord3d  6046  caovord  6047  caovord3  6049  caofrss  6126  caoftrn  6128  frxp  6241  poxp  6243  fnse  6248  brtpos2  6256  rntpos  6263  tpostpos  6270  fvopab5  6305  ertr  6691  ecopovsym  6776  ecopovtrn  6777  th3qlem2  6781  isfi  6901  en0  6940  en1  6944  endisj  6965  xpcomco  6968  sbth  6997  2pwne  7033  disjenex  7035  ssenen  7051  nneneq  7060  php  7061  sdom1  7078  isinf  7092  fineqvlem  7093  pssnn  7097  enp1i  7109  findcard  7113  findcard2  7114  findcard3  7116  frfi  7118  fiint  7149  marypha1lem  7202  supmo  7219  eqsup  7223  supub  7226  suplub  7227  supmaxlem  7231  suppr  7235  supisolem  7237  supisoex  7238  ordtypecbv  7248  ordtypelem3  7251  ordtypelem6  7254  ordtypelem7  7255  ordtypelem9  7257  ordtypelem10  7258  hartogslem1  7273  hartogs  7275  wemaplem1  7277  wemaplem2  7278  card2on  7284  card2inf  7285  elharval  7293  brwdom2  7303  wdomtr  7305  cantnfp1lem2  7397  cantnflem1  7407  wemapwe  7416  r111  7463  kardex  7580  karden  7581  isnumi  7595  tskwe  7599  cardid2  7602  cardonle  7606  cardne  7614  iscard2  7625  infxpenlem  7657  fodomfi2  7703  wdomfil  7704  wdomnumr  7707  alephsuc2  7723  infenaleph  7734  iunfictbso  7757  infpss  7859  cff1  7900  cfslb2n  7910  sornom  7919  fin4i  7940  isfin6  7942  isfin7  7943  isfin1-3  8028  fin1a2lem9  8050  fin1a2lem11  8052  hsmexlem4  8071  axcc2lem  8078  axcc4dom  8083  domtriomlem  8084  numthcor  8137  zorn2lem2  8140  zorn2lem3  8141  zorn2lem7  8145  zorn2g  8146  axdclem  8162  axdc  8164  brdom7disj  8172  brdom6disj  8173  uniimadom  8182  ondomon  8201  alephval2  8210  alephreg  8220  pwcfsdom  8221  elgch  8260  gchi  8262  fpwwe2lem12  8279  fpwwe2lem13  8280  pwfseqlem4  8300  winainflem  8331  winalim2  8334  tsken  8392  0tsk  8393  inar1  8413  tskord  8418  tskuni  8421  grudomon  8455  pinq  8567  nqereu  8569  enqeq  8574  ltbtwnnq  8618  ltrnq  8619  prcdnq  8633  prnmax  8635  genpnmax  8647  nqpr  8654  1idpr  8669  reclem2pr  8688  reclem3pr  8689  reclem4pr  8690  recexpr  8691  supexpr  8694  ltsosr  8732  1ne0sr  8734  ltasr  8738  supsrlem  8749  axpre-lttri  8803  axpre-lttrn  8804  axpre-ltadd  8805  axpre-sup  8807  lelttr  8928  ltordlem  9314  lt0ne0d  9354  fimaxre3  9719  lbreu  9720  lble  9722  lbinfm  9723  sup2  9726  infm3  9729  suprleub  9734  supmul1  9735  supmullem1  9736  supmul  9738  nnsub  9800  nominpos  9964  nnunb  9977  arch  9978  nn0sub  10030  zextle  10101  peano5uzti  10117  fzind  10126  btwnz  10130  uzval  10248  uzwo  10297  uzwoOLD  10298  nnwof  10301  uzinfmi  10313  ublbneg  10318  lbzbi  10322  zsupss  10323  uzsupss  10326  uzwo3  10327  zmax  10329  rebtwnz  10331  rpnnen1lem3  10360  xrltnsym  10487  xrlttri  10489  xrlttr  10490  xrlelttr  10503  nltpnft  10511  xrmaxlt  10526  xrmaxle  10528  qbtwnre  10542  qbtwnxr  10543  xltnegi  10559  xsubge0  10597  xlesubadd  10599  xmullem2  10601  xlemul1a  10624  xrinfmexpnf  10640  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  supxrunb1  10654  supxrunb2  10655  ixxval  10680  elixx1  10681  elioo2  10713  iccid  10717  icc0  10720  fzval  10800  elfz1  10803  flval  10942  fllelt  10945  flval2  10960  flval3  10961  flbi  10962  modid2  11010  fsequb2  11054  seqf1olem2  11102  sqlecan  11225  faclbnd4lem1  11322  sqrlem6  11749  01sqrex  11751  abslt  11814  absle  11815  rexanre  11846  rexico  11853  limsupgle  11967  limsupgre  11971  limsupbnd2  11973  rlim2lt  11987  rlim3  11988  ello12r  12007  ello1d  12013  elo12r  12018  rlimconst  12034  climshft  12066  rlimcn2  12080  o1rlimmul  12108  lo1le  12141  climsup  12159  caucvgrlem  12161  isumless  12320  divrcnv  12327  cvgrat  12355  rpnnen2lem10  12518  ruclem1  12525  ruclem2  12526  ruclem11  12534  ruclem12  12535  sqr2irr  12543  absdvdsb  12563  dvdsle  12590  dvdseq  12592  dvdsext  12595  divalglem8  12615  divalglem9  12616  divalglem10  12617  divalgmod  12621  ndvdssub  12622  sadcaddlem  12664  gcdcllem1  12706  gcdcllem2  12707  gcdcllem3  12708  gcdeq  12747  dvdssq  12755  nn0seqcvgd  12756  algcvgblem  12763  1nprm  12779  1idssfct  12780  isprm2lem  12781  isprm2  12782  dvdsprime  12787  nprm  12788  3prm  12791  dvdsprm  12794  coprm  12795  exprmfct  12805  isprm5  12807  maxprmfct  12808  eulerthlem2  12866  odzval  12872  pythagtriplem4  12888  pc2dvds  12947  pcprmpw2  12950  pcprmpw  12951  prmpwdvds  12967  pockthg  12969  unbenlem  12971  prmreclem4  12982  prmreclem5  12983  prmreclem6  12984  1arith  12990  vdwlem6  13049  vdwlem11  13054  vdwlem13  13056  ramtlecl  13063  ramub  13076  rami  13078  ramubcl  13081  0ram  13083  ram0  13085  prmlem0  13123  prmlem1a  13124  imasaddfnlem  13446  imasvscafn  13455  imasleval  13459  prslem  14081  drsdir  14085  drsdirfi  14088  isdrs2  14089  posi  14100  posasymb  14102  pltval3  14117  plelttr  14122  pospo  14123  lubprop  14130  luble  14131  lubid  14132  glbprop  14135  joinval2  14139  joinlem  14140  meetlem  14147  meetle  14150  latnlej  14190  isglbd  14237  lubub  14239  lubun  14243  clatleglb  14246  pospropd  14254  poslubmo  14266  poslubd  14267  tsrlin  14344  spwmo  14351  spwpr2  14353  spwpr4  14356  letsr  14365  dirge  14375  mndodcongi  14874  odeq  14881  odmulgeq  14886  gexnnod  14915  sylow1lem1  14925  pgpssslw  14941  sylow2a  14946  efgredeu  15077  efgred2  15078  gexex  15161  frgpnabllem2  15178  cyggenod  15187  dprdval  15254  ablfacrplem  15316  ablfac1c  15322  ablfac1eu  15324  ablfaclem3  15338  abvtrivd  15621  psrbagconcl  16135  psrbagconf1o  16136  gsumbagdiaglem  16137  psrmulcllem  16148  psrlidm  16164  psrridm  16165  psrass1  16166  psrcom  16169  mplmonmul  16224  coe1mul2  16362  coe1tmmul  16369  zlpir  16460  prmirredlem  16462  znleval  16524  ordtbas2  16937  ordtopn2  16941  ordtrest2lem  16949  pnfnei  16966  ordtt1  17123  ordthauslem  17127  2ndci  17190  2ndcsb  17191  2ndcredom  17192  2ndc1stc  17193  1stcrest  17195  2ndcctbss  17197  2ndcdisj  17198  2ndcsep  17201  lly1stc  17238  tx1stc  17360  ordthmeolem  17508  ufildom1  17637  xmetrtri2  17936  prdsxmetlem  17948  ssblex  17990  prdsbl  18053  comet  18075  stdbdxmet  18077  stdbdmopn  18080  met1stc  18083  dscmet  18111  metdstri  18371  metdscn  18376  xrhmeo  18460  bndth  18472  evth  18473  lebnumlem3  18477  pcovalg  18526  pco1  18529  pcocn  18531  pcopt  18536  pcopt2  18537  pcoass  18538  nmoleub3  18616  bcthlem5  18766  minveclem4c  18805  minveclem2  18806  minveclem3b  18808  minveclem4  18812  minveclem6  18814  pmltpclem1  18824  pmltpc  18826  ovollb2lem  18863  ovolctb  18865  ovolunlem1  18872  ovoliunlem1  18877  ovoliunlem2  18878  ovoliun2  18881  ovolshftlem1  18884  ovolscalem1  18888  ovolicc1  18891  ovolicc2lem3  18894  voliunlem2  18924  voliunlem3  18925  ioombl1lem4  18934  uniioovol  18950  uniioombllem2  18954  uniioombllem3  18956  uniioombllem6  18959  volsup2  18976  ismbfd  19011  mbfsup  19035  mbflimsup  19037  itg1climres  19085  mbfi1fseqlem4  19089  itg2lr  19101  itg2leub  19105  itg2seq  19113  itg2monolem1  19121  itg2monolem3  19123  itg2mono  19124  itg2i1fseq2  19127  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  itg2cn  19134  iblss  19175  itgless  19187  ibladdlem  19190  iblabsr  19200  iblmulc2  19201  itgabs  19205  ditgeq1  19214  dvferm2lem  19349  rolle  19353  dvlip2  19358  c1liplem1  19359  c1lip1  19360  dvfsumlem2  19390  dvfsumlem4  19392  mdegleb  19466  degltlem1  19474  plyco0  19590  plyeq0lem  19608  coeeq2  19640  dgrle  19641  dgradd2  19665  plydiveu  19694  aareccl  19722  aalioulem2  19729  aaliou3lem7  19745  psercnlem1  19817  pilem2  19844  pilem3  19845  logltb  19969  divlogrlim  19998  logcnlem3  20007  cxpaddlelem  20107  rlimcnp  20276  cxplim  20282  cxploglim  20288  scvxcvx  20296  ftalem1  20326  ftalem2  20327  isppw2  20369  vmappw  20370  sgmnncl  20401  sqff1o  20436  dvdsdivcl  20437  fsumdvdsdiaglem  20439  dvdsppwf1o  20442  dvdsflsumcom  20444  musum  20447  muinv  20449  dvdsmulf1o  20450  vmalelog  20460  vmasum  20471  logfac2  20472  perfectlem2  20485  bcmono  20532  bpos1lem  20537  bposlem9  20547  lgsmod  20576  lgsne0  20588  2sqlem6  20624  2sqlem8  20627  2sqlem10  20629  chtppilim  20640  rpvmasumlem  20652  dchrisumlema  20653  dchrisumlem2  20655  dchrvmasumlem1  20660  dchrvmasumiflem1  20666  dchrisum0flblem1  20673  dchrisum0flblem2  20674  dchrisum0  20685  rplogsum  20692  logsqvma  20707  pntpbnd1  20751  pntpbnd2  20752  pntibndlem3  20757  pntlemj  20768  pntlemi  20769  pntlem3  20774  pnt3  20777  ostth3  20803  gxnval  20943  rngosn4  21110  rngoueqz  21113  nmoubi  21366  minvecolem2  21470  minvecolem3  21471  minvecolem4c  21474  minvecolem4  21475  minvecolem5  21476  minvecolem6  21477  htthlem  21513  chlimi  21830  chcompl  21838  hsn0elch  21843  cmbr3  22203  cmcm  22209  cmcm3  22210  lecm  22212  nmopub  22504  nmfnleub  22521  nmopun  22610  nmcexi  22622  cnlnadjlem7  22669  pjnmopi  22744  stle0i  22835  stlesi  22837  stm1i  22839  csmdsymi  22930  cvmd  22932  atcveq0  22944  atcv1  22976  atord  22984  atcvat2  22985  chirred  22991  mdsym  23008  mddmdin0i  23027  cdj1i  23029  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemsv  23084  ballotlemsf1o  23088  fmptcof2  23244  isoun  23257  lt2addrd  23264  xlt2addrd  23268  xrofsup  23270  xrge0iifiso  23332  xrge0addgt0  23346  rge0scvg  23388  esumpinfval  23456  esumpcvgval  23461  esumcvg  23469  sigaclcu  23493  sigaclci  23508  unelsiga  23510  measvun  23552  orvcval2  23674  dstfrvel  23689  eupath2  23919  relexpindlem  24051  rtrclreclem.trans  24058  dedekind  24097  dedekindle  24098  faclimlem5  24121  dfdm5  24203  dfrn5  24204  trpredpred  24302  poseq  24324  nodense  24414  nocvxminlem  24415  nobnddown  24426  nofulllem4  24430  nofulllem5  24431  brpprod  24496  brsset  24500  brbigcup  24509  dffix2  24516  elfuns  24525  brimageg  24537  brdomaing  24545  brrangeg  24546  brimg  24547  brapply  24548  brsuccf  24551  funpartlem  24552  brrestrict  24559  dfrdg4  24560  axlowdim2  24660  axlowdim  24661  axcontlem2  24665  axcontlem3  24666  axcontlem4  24667  axcontlem7  24670  axcontlem9  24672  axcontlem10  24673  axcontlem11  24674  axcontlem12  24675  brofs  24700  btwncomim  24708  btwnintr  24714  btwnexch3  24715  btwnexch2  24718  brifs  24738  brcolinear2  24753  colineardim1  24756  brfs  24774  btwnconn1  24796  segcon2  24800  seglerflx  24807  seglemin  24808  btwnsegle  24812  colinbtwnle  24813  broutsideof2  24817  fvray  24836  lineunray  24842  lineelsb2  24843  linerflx1  24844  supaddc  24995  supadd  24996  ltflcei  24998  lxflflp1  25000  itg2addnclem  25003  itg2addnc  25005  itg2gt0cn  25006  ibladdnclem  25007  iblmulc2nc  25016  itgabsnc  25020  bddiblnc  25021  imgfldref2  25167  srefwref  25170  prj1b  25182  prj3  25183  oriso  25317  supdef  25365  supdefa  25366  ismxl2  25370  defse3  25375  inposet  25381  dfdir2  25394  cntrset  25705  supnuf  25732  fnctartar  26010  fnctartar2  26011  trer  26330  elicc3  26331  finminlem  26334  nn0prpwlem  26341  nn0prpw  26342  indexdom  26516  filbcmb  26535  fdc  26558  prdsbnd  26620  heiborlem3  26640  rrnequiv  26662  prtlem10  26836  lzenom  26952  fphpdo  27003  irrapxlem4  27013  pellexlem6  27022  infmrgelbi  27066  pellfundre  27069  pellfundlb  27072  monotoddzz  27131  zindbi  27134  divalgmodcl  27183  jm2.27  27204  rmydioph  27210  rpnnen3lem  27227  fnwe2lem2  27251  aomclem8  27262  hbtlem5  27435  hbt  27437  pmtrval  27497  pmtrrn  27502  pmtrfrn  27503  phisum  27621  rfcnnnub  27810  stoweidlem5  27857  stoweidlem7  27859  stoweidlem20  27872  stoweidlem26  27878  stoweidlem28  27880  stoweidlem29  27881  stoweidlem34  27886  wallispilem3  27919  stirlinglem13  27938  funressnfv  28096  dfdfat2  28099  tz6.12-afv  28141  elfznelfzo  28213  usgra1v  28260  cusgra1v  28296  isfrgra  28417  3vfriswmgra  28429  1to2vfriswmgra  28430  sgnval  28499  bnj23  29060  bnj1185  29142  bnj1152  29344  bnj1418  29386  lubunNEW  29785  lsatcveq0  29844  lsatcv1  29860  oposlem  29995  opnlen0  30000  lub0N  30001  glb0N  30005  omllaw  30055  cmtbr4N  30067  cvrval  30081  cvrnbtwn  30083  cvrnbtwn2  30087  cvrnbtwn3  30088  cvrcon3b  30089  cvrnbtwn4  30091  atcvreq0  30126  atnle  30129  atlatmstc  30131  cvlexch1  30140  glbconN  30188  hlsuprexch  30192  exatleN  30215  cvratlem  30232  atcvrj0  30239  atcvrj2b  30243  atlelt  30249  cvrat4  30254  3dim1lem5  30277  3dim2  30279  3dim3  30280  ps-2  30289  llni  30319  llnn0  30327  llnle  30329  lplni  30343  lplni2  30348  lplnle  30351  lplnn0N  30358  llncvrlpln  30369  2llnjN  30378  lvoli  30386  lvoli3  30388  lvoli2  30392  lvoln0N  30402  4at  30424  lplncvrlvol  30427  2lplnj  30431  dalemcea  30471  dalem3  30475  psubspi  30558  linepsubN  30563  elpmap  30569  pmapsub  30579  lnatexN  30590  cdlema1N  30602  cdlemb  30605  elpadd  30610  paddvaln0N  30612  paddasslem5  30635  llnexchb2lem  30679  llnexch2N  30681  islhp  30807  lhpat3  30857  4atexlemex2  30882  4atex  30887  4atex2-0aOLDN  30889  4atex2-0cOLDN  30891  lautle  30895  lautcvr  30903  lauteq  30906  ldilval  30924  ltrnu  30932  trlval2  30974  trlne  30996  cdleme0ex1N  31034  cdleme0nex  31101  cdleme18d  31106  cdlemednuN  31111  cdleme25b  31165  cdleme25cv  31169  cdleme27b  31179  cdleme29b  31186  cdleme31sn  31191  cdleme31fv  31201  cdleme31fv2  31204  cdlemefrs29bpre0  31207  cdlemefr29bpre0N  31217  cdlemefr29clN  31218  cdlemefr32fvaN  31220  cdlemefr32fva1  31221  cdlemefs29pre00N  31223  cdlemefs32sn1aw  31225  cdlemefs29bpre0N  31227  cdlemefs29bpre1N  31228  cdlemefs29cpre1N  31229  cdlemefs29clN  31230  cdlemefs32fvaN  31233  cdlemefs32fva1  31234  cdleme41sn3a  31244  cdleme32fva  31248  cdleme32e  31256  cdleme35f  31265  cdleme40v  31280  cdleme42b  31289  trlord  31380  cdlemg1cex  31399  diaval  31844  diaeldm  31848  diaelrnN  31857  cdlemm10N  31930  dibglbN  31978  dicval  31988  dicfnN  31995  dicvalrelN  31997  dihval  32044  dihlsscpre  32046  dihglblem3N  32107  dihmeetlem2N  32111  djhcvat42  32227
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator