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

Theorem breq1 4455
Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
breq1

Proof of Theorem breq1
StepHypRef Expression
1 opeq1 4217 . . 3
21eleq1d 2526 . 2
3 df-br 4453 . 2
4 df-br 4453 . 2
52, 3, 43bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  <.cop 4035   class class class wbr 4452
This theorem is referenced by:  breq12  4457  breq1i  4459  breq1d  4462  nbrne2  4470  brab1  4497  pocl  4812  swopolem  4814  swopo  4815  solin  4828  sotrieq  4832  sotr2  4834  isso2i  4837  somo  4839  frirr  4861  fr2nr  4862  wereu2  4881  vtoclr  5049  frsn  5075  brcog  5174  brcogw  5176  opelcnvg  5187  dfdmf  5201  eldmg  5203  dfrnf  5246  dfres2  5331  imasng  5364  asymref2  5389  sotri2  5401  somin1  5408  coi1  5528  dffun6f  5607  funmo  5609  fun11  5658  fveq2  5871  eliman0  5900  nfunsn  5902  dffv2  5946  fvopab5  5979  dff3  6044  f1ompt  6053  fmptco  6064  dff13  6166  foeqcnvco  6203  isorel  6222  soisores  6223  soisoi  6224  isocnv  6226  isotr  6232  isomin  6233  isoini  6234  isopolem  6241  isosolem  6243  f1oiso  6247  f1oiso2  6248  weniso  6250  caovordig  6480  caovordg  6482  caovord3d  6485  caovord  6486  caovord3  6488  caofrss  6573  caoftrn  6575  fr3nr  6615  dfwe2  6617  f1oweALT  6784  frxp  6910  poxp  6912  fnse  6917  brtpos2  6980  rntpos  6987  tpostpos  6994  ertr  7345  ecopovsym  7432  ecopovtrn  7433  isfi  7559  en0  7598  en1  7602  endisj  7624  xpcomco  7627  sbth  7657  2pwne  7693  disjenex  7695  ssenen  7711  nneneq  7720  php  7721  sdom1  7739  isinf  7753  fineqvlem  7754  pssnn  7758  en1eqsnbi  7770  enp1i  7775  findcard  7779  findcard2  7780  findcard3  7783  frfi  7785  fiint  7817  mapfienlem1  7884  mapfienlem2  7885  mapfienlem3  7886  mapfien  7887  marypha1lem  7913  supmo  7932  eqsup  7936  supub  7939  suplub  7940  supmaxlemOLD  7945  suppr  7950  supisolem  7952  supisoex  7953  ordtypecbv  7963  ordtypelem3  7966  ordtypelem6  7969  ordtypelem7  7970  ordtypelem9  7972  ordtypelem10  7973  hartogslem1  7988  hartogs  7990  wemaplem1  7992  wemaplem2  7993  wemapso2lem  7999  card2on  8001  card2inf  8002  elharval  8010  brwdom2  8020  wdomtr  8022  cantnfs  8106  cantnfp1lem2  8119  oemapso  8122  cantnflem1  8129  cantnfp1lem2OLD  8145  cantnflem1OLD  8152  wemapwe  8160  wemapweOLD  8161  r111  8214  kardex  8333  karden  8334  isnumi  8348  tskwe  8352  cardid2  8355  cardonle  8359  cardne  8367  iscard2  8378  infxpenlem  8412  fodomfi2  8462  wdomfil  8463  wdomnumr  8466  alephsuc2  8482  infenaleph  8493  iunfictbso  8516  infpss  8618  cff1  8659  cfslb2n  8669  sornom  8678  fin4i  8699  isfin6  8701  isfin7  8702  isfin1-3  8787  fin1a2lem9  8809  fin1a2lem11  8811  hsmexlem4  8830  axcc2lem  8837  axcc4dom  8842  domtriomlem  8843  numthcor  8895  zorn2lem2  8898  zorn2lem3  8899  zorn2lem7  8903  zorn2g  8904  axdclem  8920  axdc  8922  brdom7disj  8930  brdom6disj  8931  uniimadom  8940  ondomon  8959  alephval2  8968  alephreg  8978  pwcfsdom  8979  elgch  9021  gchi  9023  fpwwe2lem12  9040  fpwwe2lem13  9041  pwfseqlem4  9061  winainflem  9092  winalim2  9095  tsken  9153  0tsk  9154  inar1  9174  tskord  9179  tskuni  9182  grudomon  9216  pinq  9326  nqereu  9328  enqeq  9333  ltbtwnnq  9377  ltrnq  9378  prcdnq  9392  prnmax  9394  genpnmax  9406  nqpr  9413  1idpr  9428  reclem2pr  9447  reclem3pr  9448  reclem4pr  9449  recexpr  9450  supexpr  9453  ltsosr  9492  1ne0sr  9494  ltasr  9498  supsrlem  9509  axpre-lttri  9563  axpre-lttrn  9564  axpre-ltadd  9565  axpre-sup  9567  lelttr  9696  dedekind  9765  dedekindle  9766  ltordlem  10103  lt0ne0d  10143  fimaxre3  10517  lbreu  10518  lble  10520  sup2  10524  infm3  10527  suprleub  10532  supmul1  10533  supmullem1  10534  supmul  10536  nnsub  10599  nominpos  10800  nnunb  10816  arch  10817  nn0sub  10871  nn0n0n1ge2b  10885  nn0lt10b  10950  zextle  10961  peano5uzti  10977  fzind  10987  btwnz  10991  uzval  11112  uzwo  11173  uzwoOLD  11174  nnwof  11177  uzinfmi  11190  ublbneg  11195  lbzbi  11199  zsupss  11200  uzsupss  11203  uzwo3  11206  zmax  11208  rebtwnz  11210  rpnnen1lem3  11239  xrltnsym  11372  xrlttri  11374  xrlttr  11375  xrlelttr  11388  nltpnft  11396  xrmaxlt  11411  xrmaxle  11413  qbtwnre  11427  qbtwnxr  11428  xltnegi  11444  xsubge0  11482  xlesubadd  11484  xmullem2  11486  xlemul1a  11509  xrinfmexpnf  11526  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  supxrunb1  11540  supxrunb2  11541  ixxval  11566  elixx1  11567  elioo2  11599  iccid  11603  icc0  11606  fzval  11703  elfz1  11706  elfznelfzo  11915  elfznelfzob  11916  flval  11931  fllelt  11934  flflp1  11944  flval2  11950  flval3  11951  flbi  11952  dfceil2  11968  ceilval2  11969  fleqceilz  11981  modid2  12023  fsequb2  12086  ssnn0fi  12094  seqf1olem2  12147  sqlecan  12274  faclbnd4lem1  12371  pr2pwpr  12520  swrdccatid  12722  sgnval  12921  sqrlem6  13081  01sqrex  13083  abslt  13147  absle  13148  rexanre  13179  rexico  13186  limsupgle  13300  limsupgre  13304  limsupbnd2  13306  rlim2lt  13320  rlim3  13321  ello12r  13340  ello1d  13346  elo12r  13351  rlimconst  13367  climshft  13399  rlimcn2  13413  o1rlimmul  13441  lo1le  13474  climsup  13492  caucvgrlem  13495  isumless  13657  divrcnv  13664  cvgrat  13692  rpnnen2lem10  13957  ruclem1  13964  ruclem2  13965  ruclem11  13973  ruclem12  13974  sqrt2irr  13982  absdvdsb  14002  dvdsle  14031  dvdseq  14033  dvdsext  14037  divalglem8  14058  divalglem9  14059  divalglem10  14060  divalgmod  14064  ndvdssub  14065  sadcaddlem  14107  gcdcllem1  14149  gcdcllem2  14150  gcdcllem3  14151  gcdeq  14190  dvdssq  14198  nn0seqcvgd  14199  algcvgblem  14206  1nprm  14222  1idssfct  14223  isprm2lem  14224  isprm2  14225  dvdsprime  14230  nprm  14231  3prm  14234  dvdsprm  14240  coprm  14241  exprmfct  14251  isprm5  14253  maxprmfct  14254  eulerthlem2  14312  odzval  14318  pythagtriplem4  14343  pc2dvds  14402  pcprmpw2  14405  pcprmpw  14406  prmpwdvds  14422  pockthg  14424  unbenlem  14426  prmreclem4  14437  prmreclem5  14438  prmreclem6  14439  1arith  14445  vdwlem6  14504  vdwlem11  14509  vdwlem13  14511  ramtlecl  14518  ramub  14531  rami  14533  ramubcl  14536  0ram  14538  ram0  14540  prmlem0  14591  prmlem1a  14592  imasaddfnlem  14925  imasvscafn  14934  imasleval  14938  prslem  15560  drsdir  15564  drsdirfi  15567  isdrs2  15568  posi  15579  posasymb  15582  pltval3  15597  plelttr  15602  pospo  15603  lubprop  15616  luble  15617  lublecllem  15618  glbprop  15629  joinval2lem  15638  joinlem  15641  meetlem  15655  meetle  15658  latnlej  15698  isglbd  15747  lubub  15749  lubun  15753  clatleglb  15756  pospropd  15764  poslubmo  15776  posglbmo  15777  poslubd  15778  tsrlin  15849  letsr  15857  dirge  15867  pmtrval  16476  pmtrrn  16482  pmtrfrn  16483  pmtrrn2  16485  pmtrsn  16544  mndodcongi  16567  odeq  16574  odmulgeq  16579  gexnnod  16608  sylow1lem1  16618  pgpssslw  16634  sylow2a  16639  efgredeu  16770  efgred2  16771  gexex  16859  frgpnabllem2  16878  cyggenod  16887  dprdval  17034  dprdvalOLD  17036  dprdw  17043  dprdwd  17044  ablfacrplem  17116  ablfac1c  17122  ablfac1eu  17124  ablfaclem3  17138  abvtrivd  17489  psrbagconcl  18025  psrbagconf1o  18026  gsumbagdiaglem  18027  psrmulcllem  18040  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  psrass1  18060  psrcom  18064  mplelbas  18087  mplmonmul  18126  ltbwe  18137  coe1fsupp  18254  coe1ae0  18257  coe1mul2  18310  coe1tmmul  18318  zringlpir  18512  zlpir  18517  prmirredlem  18523  prmirredlemOLD  18526  znleval  18593  frlmelbas  18788  ellspd  18836  islindf4  18873  pmatcoe1fsupp  19202  chfacffsupp  19357  chfacfscmulfsupp  19360  chfacfscmulgsum  19361  chfacfpmmulfsupp  19364  chfacfpmmulgsum  19365  ordtbas2  19692  ordtopn2  19696  ordtrest2lem  19704  pnfnei  19721  ordtt1  19880  ordthauslem  19884  2ndci  19949  2ndcsb  19950  2ndcredom  19951  2ndc1stc  19952  1stcrest  19954  2ndcctbss  19956  2ndcdisj  19957  2ndcsep  19960  lly1stc  19997  tx1stc  20151  ordthmeolem  20302  ufildom1  20427  xmetrtri2  20859  prdsxmetlem  20871  ssblex  20931  prdsbl  20994  comet  21016  stdbdxmet  21018  stdbdmopn  21021  met1stc  21024  dscmet  21093  metdstri  21355  metdscn  21360  xrhmeo  21446  bndth  21458  evth  21459  lebnumlem3  21463  pcovalg  21512  pco1  21515  pcocn  21517  pcopt  21522  pcopt2  21523  pcoass  21524  nmoleub3  21602  bcthlem5  21767  rrxfsupp  21829  minveclem4c  21840  minveclem2  21841  minveclem3b  21843  minveclem4  21847  minveclem6  21849  pmltpclem1  21860  pmltpc  21862  ovollb2lem  21899  ovolctb  21901  ovolunlem1  21908  ovoliunlem1  21913  ovoliunlem2  21914  ovoliun2  21917  ovolshftlem1  21920  ovolscalem1  21924  ovolicc1  21927  ovolicc2lem3  21930  voliunlem2  21961  voliunlem3  21962  ioombl1lem4  21971  uniioovol  21988  uniioombllem2  21992  uniioombllem3  21994  uniioombllem6  21997  volsup2  22014  ismbfd  22047  mbfsup  22071  mbflimsup  22073  itg1climres  22121  mbfi1fseqlem4  22125  itg2lr  22137  itg2leub  22141  itg2seq  22149  itg2monolem1  22157  itg2monolem3  22159  itg2mono  22160  itg2i1fseq2  22163  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  itg2cn  22170  iblss  22211  itgless  22223  ibladdlem  22226  iblabsr  22236  iblmulc2  22237  itgabs  22241  ditgeq1  22252  dvferm2lem  22387  rolle  22391  dvlip2  22396  c1liplem1  22397  c1lip1  22398  dvfsumlem2  22428  dvfsumlem4  22430  mdegleb  22464  degltlem1  22472  plyco0  22589  plyeq0lem  22607  coeeq2  22639  dgrle  22640  dgradd2  22665  plydiveu  22694  aareccl  22722  aalioulem2  22729  aaliou3lem7  22745  psercnlem1  22820  pilem2  22847  pilem3  22848  logltb  22984  divlogrlim  23016  logcnlem3  23025  cxpaddlelem  23125  rlimcnp  23295  cxplim  23301  cxploglim  23307  scvxcvx  23315  ftalem1  23346  ftalem2  23347  isppw2  23389  vmappw  23390  sgmnncl  23421  sqff1o  23456  dvdsdivcl  23457  fsumdvdsdiaglem  23459  dvdsppwf1o  23462  dvdsflsumcom  23464  musum  23467  muinv  23469  dvdsmulf1o  23470  vmalelog  23480  vmasum  23491  logfac2  23492  perfectlem2  23505  bcmono  23552  bpos1lem  23557  bposlem9  23567  lgsmod  23596  lgsne0  23608  2sqlem6  23644  2sqlem8  23647  2sqlem10  23649  chtppilim  23660  rpvmasumlem  23672  dchrisumlema  23673  dchrisumlem2  23675  dchrvmasumlem1  23680  dchrvmasumiflem1  23686  dchrisum0flblem1  23693  dchrisum0flblem2  23694  dchrisum0  23705  rplogsum  23712  logsqvma  23727  pntpbnd1  23771  pntpbnd2  23772  pntibndlem3  23777  pntlemj  23788  pntlemi  23789  pntlem3  23794  pnt3  23797  ostth3  23823  lmif  24151  islmib  24153  axlowdim2  24263  axlowdim  24264  axcontlem2  24268  axcontlem3  24269  axcontlem4  24270  axcontlem7  24273  axcontlem9  24275  axcontlem10  24276  axcontlem11  24277  axcontlem12  24278  ebtwntg  24285  usgra1v  24390  usgrafisindb0  24408  usgrafisindb1  24409  cusgra1v  24461  1conngra  24675  clwlkisclwwlklem2fv1  24782  clwlkf1clwwlklem1  24846  isrusgusrgcl  24933  isrgrac  24934  0eusgraiff0rgracl  24941  eupath2  24980  isfrgra  24990  3vfriswmgra  25005  1to2vfriswmgra  25006  vdfrgra0  25022  numclwwlk5  25112  frgraregord013  25118  gxnval  25262  rngoueqz  25432  nmoubi  25687  minvecolem2  25791  minvecolem3  25792  minvecolem4c  25795  minvecolem4  25796  minvecolem5  25797  minvecolem6  25798  htthlem  25834  chlimi  26152  chcompl  26160  hsn0elch  26166  cmbr3  26526  cmcm  26532  cmcm3  26533  lecm  26535  nmopub  26827  nmfnleub  26844  nmopun  26933  nmcexi  26945  cnlnadjlem7  26992  pjnmopi  27067  stle0i  27158  stlesi  27160  stm1i  27162  csmdsymi  27253  cvmd  27255  atcveq0  27267  atcv1  27299  atord  27307  atcvat2  27308  chirred  27314  mdsym  27331  mddmdin0i  27350  cdj1i  27352  fmptcof2  27502  isoun  27520  fcobijfs  27549  lt2addrd  27563  xlt2addrd  27578  xrge0infss  27580  xrofsup  27582  tleile  27649  toslublem  27655  tosglblem  27657  omndadd  27696  xrnarchi  27728  archirng  27732  archiexdiv  27734  archiabl  27742  isarchiofld  27807  cmpcref  27853  ldlfcntref  27857  dispcmp  27862  ordtrest2NEWlem  27904  ordtconlem1  27906  xrge0iifiso  27917  rge0scvg  27931  gsumesum  28067  esumfsup  28076  esumpinfval  28079  esumpcvgval  28084  esumcvg  28092  sigaclcu  28117  sigaclci  28132  unelsiga  28134  measvun  28180  voliune  28201  volfiniune  28202  oms0  28266  orvcval2  28397  dstfrvel  28412  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemsv  28448  ballotlemsf1o  28452  sgnmulsgn  28488  relexpindlem  29062  rtrclreclem.trans  29069  dfdm5  29206  dfrn5  29207  trpredpred  29311  poseq  29333  wsuclem  29381  nodense  29449  nocvxminlem  29450  nobnddown  29461  nofulllem4  29465  nofulllem5  29466  brpprod  29535  brsset  29539  brbigcup  29548  dffix2  29555  elfuns  29565  brimageg  29577  brdomaing  29585  brrangeg  29586  brimg  29587  brapply  29588  brsuccf  29591  funpartlem  29592  brrestrict  29599  dfrdg4  29600  brofs  29655  btwncomim  29663  btwnintr  29669  btwnexch3  29670  btwnexch2  29673  brifs  29693  brcolinear2  29708  colineardim1  29711  brfs  29729  btwnconn1  29751  segcon2  29755  seglerflx  29762  seglemin  29763  btwnsegle  29767  colinbtwnle  29768  broutsideof2  29772  fvray  29791  lineunray  29797  lineelsb2  29798  linerflx1  29799  fin2solem  30039  fin2so  30040  supaddc  30041  supadd  30042  ltflcei  30043  heicant  30049  mblfinlem1  30051  mblfinlem2  30052  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  ibladdnclem  30071  iblmulc2nc  30080  itgabsnc  30084  bddiblnc  30085  ftc1anclem5  30094  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  trer  30134  elicc3  30135  finminlem  30136  nn0prpwlem  30140  nn0prpw  30141  fnessref  30175  refssfne  30176  indexdom  30225  filbcmb  30231  fdc  30238  prdsbnd  30289  heiborlem3  30309  rrnequiv  30331  prtlem10  30606  lzenom  30703  fphpdo  30751  irrapxlem4  30761  pellexlem6  30770  infmrgelbi  30814  pellfundre  30817  pellfundlb  30820  monotoddzz  30879  zindbi  30882  divalgmodcl  30929  jm2.27  30950  rmydioph  30956  rpnnen3lem  30973  fnwe2lem2  30997  aomclem8  31007  hbtlem5  31077  hbt  31079  phisum  31159  lcmval  31198  lcmdvds  31214  lcmgcdeq  31216  nzss  31222  dstregt0  31463  limsupre  31647  icccncfext  31690  cncficcgt0  31691  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  stoweidlem5  31787  stoweidlem20  31802  stoweidlem26  31808  stoweidlem28  31810  stoweidlem29  31811  stoweidlem34  31816  wallispilem3  31849  stirlinglem13  31868  fourierdlem41  31930  fourierdlem42  31931  fourierdlem51  31940  fourierdlem54  31943  funressnfv  32213  dfdfat2  32216  tz6.12-afv  32258  usgo0s0  32435  usgo0s0ALT  32436  usgo1s0ALT  32437  usgo1s0  32442  assintop  32533  isassintop  32534  assintopcllaw  32536  ztprmneprm  32936  ply1mulgsumlem1  32986  ply1mulgsumlem2  32987  lco0  33028  lcoel0  33029  lincsumcl  33032  lincscmcl  33033  lcoss  33037  linindslinci  33049  lindslinindsimp1  33058  linds0  33066  el0ldep  33067  lindsrng01  33069  ldepspr  33074  islindeps2  33084  isldepslvec2  33086  zlmodzxzldep  33105  ldepsnlinc  33109  bnj23  33771  bnj1185  33852  bnj1152  34054  bnj1418  34096  lsatcveq0  34757  lsatcv1  34773  oposlem  34907  opnlen0  34913  lub0N  34914  glb0N  34918  omllaw  34968  cmtbr4N  34980  cvrval  34994  cvrnbtwn  34996  cvrnbtwn2  35000  cvrnbtwn3  35001  cvrcon3b  35002  cvrnbtwn4  35004  atcvreq0  35039  atnle  35042  atlatmstc  35044  cvlexch1  35053  glbconN  35101  hlsuprexch  35105  exatleN  35128  cvratlem  35145  atcvrj0  35152  atcvrj2b  35156  atlelt  35162  cvrat4  35167  3dim1lem5  35190  3dim2  35192  3dim3  35193  ps-2  35202  llni  35232  llnn0  35240  llnle  35242  lplni  35256  lplni2  35261  lplnle  35264  lplnn0N  35271  llncvrlpln  35282  2llnjN  35291  lvoli  35299  lvoli3  35301  lvoli2  35305  lvoln0N  35315  4at  35337  lplncvrlvol  35340  2lplnj  35344  dalemcea  35384  dalem3  35388  psubspi  35471  linepsubN  35476  elpmap  35482  pmapsub  35492  lnatexN  35503  cdlema1N  35515  cdlemb  35518  elpadd  35523  paddvaln0N  35525  paddasslem5  35548  llnexchb2lem  35592  llnexch2N  35594  islhp  35720  lhpat3  35770  4atexlemex2  35795  4atex  35800  4atex2-0aOLDN  35802  4atex2-0cOLDN  35804  lautle  35808  lautcvr  35816  lauteq  35819  ldilval  35837  ltrnu  35845  trlval2  35888  trlne  35910  cdleme0ex1N  35948  cdleme0nex  36015  cdleme18d  36020  cdlemednuN  36025  cdleme25b  36080  cdleme25cv  36084  cdleme27b  36094  cdleme29b  36101  cdleme31sn  36106  cdleme31fv  36116  cdleme31fv2  36119  cdlemefrs29bpre0  36122  cdlemefr29bpre0N  36132  cdlemefr29clN  36133  cdlemefr32fvaN  36135  cdlemefr32fva1  36136  cdlemefs29pre00N  36138  cdlemefs32sn1aw  36140  cdlemefs29bpre0N  36142  cdlemefs29bpre1N  36143  cdlemefs29cpre1N  36144  cdlemefs29clN  36145  cdlemefs32fvaN  36148  cdlemefs32fva1  36149  cdleme41sn3a  36159  cdleme32fva  36163  cdleme32e  36171  cdleme35f  36180  cdleme40v  36195  cdleme42b  36204  trlord  36295  cdlemg1cex  36314  diaval  36759  diaeldm  36763  diaelrnN  36772  cdlemm10N  36845  dibglbN  36893  dicval  36903  dicfnN  36910  dicvalrelN  36912  dihval  36959  dihlsscpre  36961  dihglblem3N  37022  dihmeetlem2N  37026  djhcvat42  37142  taupilemrplb  37695  frege70  37961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator