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

Theorem breq1 4026
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 3796 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2349 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 4024 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 4024 . 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 1623    e. wcel 1684   <.cop 3643   class class class wbr 4023
This theorem is referenced by:  breq12  4028  breq1i  4030  breq1d  4033  nbrne2  4041  brab1  4068  pocl  4321  swopolem  4323  swopo  4324  solin  4337  sotrieq  4341  sotr2  4343  isso2i  4346  somo  4348  frirr  4370  fr2nr  4371  wereu2  4390  fr3nr  4571  dfwe2  4573  vtoclr  4733  frsn  4760  brcog  4850  opelcnvg  4861  dfdmf  4873  eldmg  4874  dfrnf  4917  dfres2  5002  imasng  5035  asymref2  5060  sotri2  5072  somin1  5079  coi1  5188  dffun6f  5269  funmo  5271  fun11  5315  fveq2  5525  nfunsn  5558  dffv2  5592  dff3  5673  f1ompt  5682  fmptco  5691  dff13  5783  foeqcnvco  5804  isorel  5823  soisores  5824  soisoi  5825  isocnv  5827  isotr  5833  isomin  5834  isoini  5835  isopolem  5842  isosolem  5844  f1oiso  5848  f1oiso2  5849  f1oweALT  5851  weniso  5852  caovordig  6025  caovordg  6027  caovord3d  6030  caovord  6031  caovord3  6033  caofrss  6110  caoftrn  6112  frxp  6225  poxp  6227  fnse  6232  brtpos2  6240  rntpos  6247  tpostpos  6254  fvopab5  6289  ertr  6675  ecopovsym  6760  ecopovtrn  6761  th3qlem2  6765  isfi  6885  en0  6924  en1  6928  endisj  6949  xpcomco  6952  sbth  6981  2pwne  7017  disjenex  7019  ssenen  7035  nneneq  7044  php  7045  sdom1  7062  isinf  7076  fineqvlem  7077  pssnn  7081  enp1i  7093  findcard  7097  findcard2  7098  findcard3  7100  frfi  7102  fiint  7133  marypha1lem  7186  supmo  7203  eqsup  7207  supub  7210  suplub  7211  supmaxlem  7215  suppr  7219  supisolem  7221  supisoex  7222  ordtypecbv  7232  ordtypelem3  7235  ordtypelem6  7238  ordtypelem7  7239  ordtypelem9  7241  ordtypelem10  7242  hartogslem1  7257  hartogs  7259  wemaplem1  7261  wemaplem2  7262  card2on  7268  card2inf  7269  elharval  7277  brwdom2  7287  wdomtr  7289  cantnfp1lem2  7381  cantnflem1  7391  wemapwe  7400  r111  7447  kardex  7564  karden  7565  isnumi  7579  tskwe  7583  cardid2  7586  cardonle  7590  cardne  7598  iscard2  7609  infxpenlem  7641  fodomfi2  7687  wdomfil  7688  wdomnumr  7691  alephsuc2  7707  infenaleph  7718  iunfictbso  7741  infpss  7843  cff1  7884  cfslb2n  7894  sornom  7903  fin4i  7924  isfin6  7926  isfin7  7927  isfin1-3  8012  fin1a2lem9  8034  fin1a2lem11  8036  hsmexlem4  8055  axcc2lem  8062  axcc4dom  8067  domtriomlem  8068  numthcor  8121  zorn2lem2  8124  zorn2lem3  8125  zorn2lem7  8129  zorn2g  8130  axdclem  8146  axdc  8148  brdom7disj  8156  brdom6disj  8157  uniimadom  8166  ondomon  8185  alephval2  8194  alephreg  8204  pwcfsdom  8205  elgch  8244  gchi  8246  fpwwe2lem12  8263  fpwwe2lem13  8264  pwfseqlem4  8284  winainflem  8315  winalim2  8318  tsken  8376  0tsk  8377  inar1  8397  tskord  8402  tskuni  8405  grudomon  8439  pinq  8551  nqereu  8553  enqeq  8558  ltbtwnnq  8602  ltrnq  8603  prcdnq  8617  prnmax  8619  genpnmax  8631  nqpr  8638  1idpr  8653  reclem2pr  8672  reclem3pr  8673  reclem4pr  8674  recexpr  8675  supexpr  8678  ltsosr  8716  1ne0sr  8718  ltasr  8722  supsrlem  8733  axpre-lttri  8787  axpre-lttrn  8788  axpre-ltadd  8789  axpre-sup  8791  lelttr  8912  ltordlem  9298  lt0ne0d  9338  fimaxre3  9703  lbreu  9704  lble  9706  lbinfm  9707  sup2  9710  infm3  9713  suprleub  9718  supmul1  9719  supmullem1  9720  supmul  9722  nnsub  9784  nominpos  9948  nnunb  9961  arch  9962  nn0sub  10014  zextle  10085  peano5uzti  10101  fzind  10110  btwnz  10114  uzval  10232  uzwo  10281  uzwoOLD  10282  nnwof  10285  uzinfmi  10297  ublbneg  10302  lbzbi  10306  zsupss  10307  uzsupss  10310  uzwo3  10311  zmax  10313  rebtwnz  10315  rpnnen1lem3  10344  xrltnsym  10471  xrlttri  10473  xrlttr  10474  xrlelttr  10487  nltpnft  10495  xrmaxlt  10510  xrmaxle  10512  qbtwnre  10526  qbtwnxr  10527  xltnegi  10543  xsubge0  10581  xlesubadd  10583  xmullem2  10585  xlemul1a  10608  xrinfmexpnf  10624  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  supxrunb1  10638  supxrunb2  10639  ixxval  10664  elixx1  10665  elioo2  10697  iccid  10701  icc0  10704  fzval  10784  elfz1  10787  flval  10926  fllelt  10929  flval2  10944  flval3  10945  flbi  10946  modid2  10994  fsequb2  11038  seqf1olem2  11086  sqlecan  11209  faclbnd4lem1  11306  sqrlem6  11733  01sqrex  11735  abslt  11798  absle  11799  rexanre  11830  rexico  11837  limsupgle  11951  limsupgre  11955  limsupbnd2  11957  rlim2lt  11971  rlim3  11972  ello12r  11991  ello1d  11997  elo12r  12002  rlimconst  12018  climshft  12050  rlimcn2  12064  o1rlimmul  12092  lo1le  12125  climsup  12143  caucvgrlem  12145  isumless  12304  divrcnv  12311  cvgrat  12339  rpnnen2lem10  12502  ruclem1  12509  ruclem2  12510  ruclem11  12518  ruclem12  12519  sqr2irr  12527  absdvdsb  12547  dvdsle  12574  dvdseq  12576  dvdsext  12579  divalglem8  12599  divalglem9  12600  divalglem10  12601  divalgmod  12605  ndvdssub  12606  sadcaddlem  12648  gcdcllem1  12690  gcdcllem2  12691  gcdcllem3  12692  gcdeq  12731  dvdssq  12739  nn0seqcvgd  12740  algcvgblem  12747  1nprm  12763  1idssfct  12764  isprm2lem  12765  isprm2  12766  dvdsprime  12771  nprm  12772  3prm  12775  dvdsprm  12778  coprm  12779  exprmfct  12789  isprm5  12791  maxprmfct  12792  eulerthlem2  12850  odzval  12856  pythagtriplem4  12872  pc2dvds  12931  pcprmpw2  12934  pcprmpw  12935  prmpwdvds  12951  pockthg  12953  unbenlem  12955  prmreclem4  12966  prmreclem5  12967  prmreclem6  12968  1arith  12974  vdwlem6  13033  vdwlem11  13038  vdwlem13  13040  ramtlecl  13047  ramub  13060  rami  13062  ramubcl  13065  0ram  13067  ram0  13069  prmlem0  13107  prmlem1a  13108  imasaddfnlem  13430  imasvscafn  13439  imasleval  13443  prslem  14065  drsdir  14069  drsdirfi  14072  isdrs2  14073  posi  14084  posasymb  14086  pltval3  14101  plelttr  14106  pospo  14107  lubprop  14114  luble  14115  lubid  14116  glbprop  14119  joinval2  14123  joinlem  14124  meetlem  14131  meetle  14134  latnlej  14174  isglbd  14221  lubub  14223  lubun  14227  clatleglb  14230  pospropd  14238  poslubmo  14250  poslubd  14251  tsrlin  14328  spwmo  14335  spwpr2  14337  spwpr4  14340  letsr  14349  dirge  14359  mndodcongi  14858  odeq  14865  odmulgeq  14870  gexnnod  14899  sylow1lem1  14909  pgpssslw  14925  sylow2a  14930  efgredeu  15061  efgred2  15062  gexex  15145  frgpnabllem2  15162  cyggenod  15171  dprdval  15238  ablfacrplem  15300  ablfac1c  15306  ablfac1eu  15308  ablfaclem3  15322  abvtrivd  15605  psrbagconcl  16119  psrbagconf1o  16120  gsumbagdiaglem  16121  psrmulcllem  16132  psrlidm  16148  psrridm  16149  psrass1  16150  psrcom  16153  mplmonmul  16208  coe1mul2  16346  coe1tmmul  16353  zlpir  16444  prmirredlem  16446  znleval  16508  ordtbas2  16921  ordtopn2  16925  ordtrest2lem  16933  pnfnei  16950  ordtt1  17107  ordthauslem  17111  2ndci  17174  2ndcsb  17175  2ndcredom  17176  2ndc1stc  17177  1stcrest  17179  2ndcctbss  17181  2ndcdisj  17182  2ndcsep  17185  lly1stc  17222  tx1stc  17344  ordthmeolem  17492  ufildom1  17621  xmetrtri2  17920  prdsxmetlem  17932  ssblex  17974  prdsbl  18037  comet  18059  stdbdxmet  18061  stdbdmopn  18064  met1stc  18067  dscmet  18095  metdstri  18355  metdscn  18360  xrhmeo  18444  bndth  18456  evth  18457  lebnumlem3  18461  pcovalg  18510  pco1  18513  pcocn  18515  pcopt  18520  pcopt2  18521  pcoass  18522  nmoleub3  18600  bcthlem5  18750  minveclem4c  18789  minveclem2  18790  minveclem3b  18792  minveclem4  18796  minveclem6  18798  pmltpclem1  18808  pmltpc  18810  ovollb2lem  18847  ovolctb  18849  ovolunlem1  18856  ovoliunlem1  18861  ovoliunlem2  18862  ovoliun2  18865  ovolshftlem1  18868  ovolscalem1  18872  ovolicc1  18875  ovolicc2lem3  18878  voliunlem2  18908  voliunlem3  18909  ioombl1lem4  18918  uniioovol  18934  uniioombllem2  18938  uniioombllem3  18940  uniioombllem6  18943  volsup2  18960  ismbfd  18995  mbfsup  19019  mbflimsup  19021  itg1climres  19069  mbfi1fseqlem4  19073  itg2lr  19085  itg2leub  19089  itg2seq  19097  itg2monolem1  19105  itg2monolem3  19107  itg2mono  19108  itg2i1fseq2  19111  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  itg2cn  19118  iblss  19159  itgless  19171  ibladdlem  19174  iblabsr  19184  iblmulc2  19185  itgabs  19189  ditgeq1  19198  dvferm2lem  19333  rolle  19337  dvlip2  19342  c1liplem1  19343  c1lip1  19344  dvfsumlem2  19374  dvfsumlem4  19376  mdegleb  19450  degltlem1  19458  plyco0  19574  plyeq0lem  19592  coeeq2  19624  dgrle  19625  dgradd2  19649  plydiveu  19678  aareccl  19706  aalioulem2  19713  aaliou3lem7  19729  psercnlem1  19801  pilem2  19828  pilem3  19829  logltb  19953  divlogrlim  19982  logcnlem3  19991  cxpaddlelem  20091  rlimcnp  20260  cxplim  20266  cxploglim  20272  scvxcvx  20280  ftalem1  20310  ftalem2  20311  isppw2  20353  vmappw  20354  sgmnncl  20385  sqff1o  20420  dvdsdivcl  20421  fsumdvdsdiaglem  20423  dvdsppwf1o  20426  dvdsflsumcom  20428  musum  20431  muinv  20433  dvdsmulf1o  20434  vmalelog  20444  vmasum  20455  logfac2  20456  perfectlem2  20469  bcmono  20516  bpos1lem  20521  bposlem9  20531  lgsmod  20560  lgsne0  20572  2sqlem6  20608  2sqlem8  20611  2sqlem10  20613  chtppilim  20624  rpvmasumlem  20636  dchrisumlema  20637  dchrisumlem2  20639  dchrvmasumlem1  20644  dchrvmasumiflem1  20650  dchrisum0flblem1  20657  dchrisum0flblem2  20658  dchrisum0  20669  rplogsum  20676  logsqvma  20691  pntpbnd1  20735  pntpbnd2  20736  pntibndlem3  20741  pntlemj  20752  pntlemi  20753  pntlem3  20758  pnt3  20761  ostth3  20787  gxnval  20927  rngosn4  21094  rngoueqz  21097  nmoubi  21350  minvecolem2  21454  minvecolem3  21455  minvecolem4c  21458  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  htthlem  21497  chlimi  21814  chcompl  21822  hsn0elch  21827  cmbr3  22187  cmcm  22193  cmcm3  22194  lecm  22196  nmopub  22488  nmfnleub  22505  nmopun  22594  nmcexi  22606  cnlnadjlem7  22653  pjnmopi  22728  stle0i  22819  stlesi  22821  stm1i  22823  csmdsymi  22914  cvmd  22916  atcveq0  22928  atcv1  22960  atord  22968  atcvat2  22969  chirred  22975  mdsym  22992  mddmdin0i  23011  cdj1i  23013  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsv  23068  ballotlemsf1o  23072  fmptcof2  23229  isoun  23242  lt2addrd  23249  xlt2addrd  23253  xrofsup  23255  xrge0iifiso  23317  xrge0addgt0  23331  rge0scvg  23373  esumpinfval  23441  esumpcvgval  23446  esumcvg  23454  sigaclcu  23478  sigaclci  23493  unelsiga  23495  measvun  23537  orvcval2  23659  dstfrvel  23674  eupath2  23904  relexpindlem  24036  rtrclreclem.trans  24043  dedekind  24082  dedekindle  24083  dfdm5  24132  dfrn5  24133  trpredpred  24231  poseq  24253  nodense  24343  nocvxminlem  24344  nobnddown  24355  nofulllem4  24359  nofulllem5  24360  brpprod  24425  brsset  24429  brbigcup  24438  dffix2  24445  elfuns  24454  brimageg  24466  brdomaing  24474  brrangeg  24475  brimg  24476  brapply  24477  brsuccf  24480  funpartfv  24483  brrestrict  24487  dfrdg4  24488  axlowdim2  24588  axlowdim  24589  axcontlem2  24593  axcontlem3  24594  axcontlem4  24595  axcontlem7  24598  axcontlem9  24600  axcontlem10  24601  axcontlem11  24602  axcontlem12  24603  brofs  24628  btwncomim  24636  btwnintr  24642  btwnexch3  24643  btwnexch2  24646  brifs  24666  brcolinear2  24681  colineardim1  24684  brfs  24702  btwnconn1  24724  segcon2  24728  seglerflx  24735  seglemin  24736  btwnsegle  24740  colinbtwnle  24741  broutsideof2  24745  fvray  24764  lineunray  24770  lineelsb2  24771  linerflx1  24772  imgfldref2  25064  srefwref  25067  prj1b  25079  prj3  25080  oriso  25214  supdef  25262  supdefa  25263  ismxl2  25267  defse3  25272  inposet  25278  dfdir2  25291  cntrset  25602  supnuf  25629  fnctartar  25907  fnctartar2  25908  trer  26227  elicc3  26228  finminlem  26231  nn0prpwlem  26238  nn0prpw  26239  indexdom  26413  filbcmb  26432  fdc  26455  prdsbnd  26517  heiborlem3  26537  rrnequiv  26559  prtlem10  26733  lzenom  26849  fphpdo  26900  irrapxlem4  26910  pellexlem6  26919  infmrgelbi  26963  pellfundre  26966  pellfundlb  26969  monotoddzz  27028  zindbi  27031  divalgmodcl  27080  jm2.27  27101  rmydioph  27107  rpnnen3lem  27124  fnwe2lem2  27148  aomclem8  27159  hbtlem5  27332  hbt  27334  pmtrval  27394  pmtrrn  27399  pmtrfrn  27400  phisum  27518  rfcnnnub  27707  stoweidlem5  27754  stoweidlem7  27756  stoweidlem20  27769  stoweidlem26  27775  stoweidlem28  27777  stoweidlem29  27778  stoweidlem34  27783  wallispilem3  27816  stirlinglem13  27835  funressnfv  27991  dfdfat2  27994  tz6.12-afv  28035  usgra1v  28126  cusgra1v  28157  isfrgra  28171  3vfriswmgra  28183  1to2vfriswmgra  28184  sgnval  28245  bnj23  28744  bnj1185  28826  bnj1152  29028  bnj1418  29070  lubunNEW  29163  lsatcveq0  29222  lsatcv1  29238  oposlem  29373  opnlen0  29378  lub0N  29379  glb0N  29383  omllaw  29433  cmtbr4N  29445  cvrval  29459  cvrnbtwn  29461  cvrnbtwn2  29465  cvrnbtwn3  29466  cvrcon3b  29467  cvrnbtwn4  29469  atcvreq0  29504  atnle  29507  atlatmstc  29509  cvlexch1  29518  glbconN  29566  hlsuprexch  29570  exatleN  29593  cvratlem  29610  atcvrj0  29617  atcvrj2b  29621  atlelt  29627  cvrat4  29632  3dim1lem5  29655  3dim2  29657  3dim3  29658  ps-2  29667  llni  29697  llnn0  29705  llnle  29707  lplni  29721  lplni2  29726  lplnle  29729  lplnn0N  29736  llncvrlpln  29747  2llnjN  29756  lvoli  29764  lvoli3  29766  lvoli2  29770  lvoln0N  29780  4at  29802  lplncvrlvol  29805  2lplnj  29809  dalemcea  29849  dalem3  29853  psubspi  29936  linepsubN  29941  elpmap  29947  pmapsub  29957  lnatexN  29968  cdlema1N  29980  cdlemb  29983  elpadd  29988  paddvaln0N  29990  paddasslem5  30013  llnexchb2lem  30057  llnexch2N  30059  islhp  30185  lhpat3  30235  4atexlemex2  30260  4atex  30265  4atex2-0aOLDN  30267  4atex2-0cOLDN  30269  lautle  30273  lautcvr  30281  lauteq  30284  ldilval  30302  ltrnu  30310  trlval2  30352  trlne  30374  cdleme0ex1N  30412  cdleme0nex  30479  cdleme18d  30484  cdlemednuN  30489  cdleme25b  30543  cdleme25cv  30547  cdleme27b  30557  cdleme29b  30564  cdleme31sn  30569  cdleme31fv  30579  cdleme31fv2  30582  cdlemefrs29bpre0  30585  cdlemefr29bpre0N  30595  cdlemefr29clN  30596  cdlemefr32fvaN  30598  cdlemefr32fva1  30599  cdlemefs29pre00N  30601  cdlemefs32sn1aw  30603  cdlemefs29bpre0N  30605  cdlemefs29bpre1N  30606  cdlemefs29cpre1N  30607  cdlemefs29clN  30608  cdlemefs32fvaN  30611  cdlemefs32fva1  30612  cdleme41sn3a  30622  cdleme32fva  30626  cdleme32e  30634  cdleme35f  30643  cdleme40v  30658  cdleme42b  30667  trlord  30758  cdlemg1cex  30777  diaval  31222  diaeldm  31226  diaelrnN  31235  cdlemm10N  31308  dibglbN  31356  dicval  31366  dicfnN  31373  dicvalrelN  31375  dihval  31422  dihlsscpre  31424  dihglblem3N  31485  dihmeetlem2N  31489  djhcvat42  31605
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator