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

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

Proof of Theorem breq2
StepHypRef Expression
1 opeq2 4218 . . 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  breq2i  4460  breq2d  4464  nbrne1  4469  pocl  4812  swopolem  4814  swopo  4815  solin  4828  sotric  4831  sotrieq  4832  isso2i  4837  somo  4839  seex  4847  frirr  4861  fr2nr  4862  frminex  4864  wereu2  4881  vtoclr  5049  posn  5073  frsn  5075  brcog  5174  brcogw  5176  opelcnvg  5187  dfdmf  5201  breldmg  5213  dfrnf  5246  dmcoss  5267  resieq  5289  dfres2  5331  elimag  5346  elrelimasn  5366  elimasn  5367  asymref2  5389  intirr  5390  poirr2  5396  sotri3  5402  poltletr  5407  soltmin  5411  dffun3  5604  dffun6f  5607  fun11  5658  brprcneu  5864  fv3  5884  tz6.12c  5890  tz6.12i  5891  funbrfv  5911  fnbrfvb  5913  funfv2f  5942  dffv2  5946  fvopab5  5979  fndmdif  5991  dff3  6044  fmptco  6064  foeqcnvco  6203  isorel  6222  soisores  6223  soisoi  6224  isocnv  6226  isotr  6232  isopolem  6241  isosolem  6243  f1oiso  6247  f1oiso2  6248  caovordig  6480  caovordg  6482  caovord  6486  caofrss  6573  caoftrn  6575  fr3nr  6615  dfwe2  6617  f1oweALT  6784  frxp  6910  poxp  6912  suppimacnv  6929  tposoprab  7010  ertr  7345  ecopovsym  7432  ecopovtrn  7433  domeng  7550  eqeng  7569  snfi  7616  sbth  7657  domunsn  7687  domssex  7698  nneneq  7720  php2  7722  onfin  7728  1sdom  7742  unxpdom  7747  isinf  7753  fineqvlem  7754  pssnn  7758  ssnnfi  7759  dif1enOLD  7772  dif1en  7773  findcard  7779  findcard2  7780  findcard3  7783  frfi  7785  fisupg  7788  nnsdomg  7799  unfi  7807  fiint  7817  mapfien2  7888  supmo  7932  eqsup  7936  supub  7939  suplub  7940  suplub2  7941  supmax  7944  supmaxlemOLD  7945  fisup2g  7947  fisupcl  7948  suppr  7950  supisolem  7952  supisoex  7953  ordtypecbv  7963  ordtypelem3  7966  ordtypelem6  7969  ordtypelem7  7970  ordtypelem9  7972  wemaplem1  7992  wemaplem2  7993  harval  8009  wemapwe  8160  wemapweOLD  8161  r111  8214  cardf2  8345  isnum2  8347  cardval3  8354  cardnueq0  8366  carden2a  8368  cardlim  8374  isinffi  8394  onsdom  8398  harval2  8399  cardmin2  8400  ondomen  8439  alephnbtwn  8473  alephinit  8497  aceq3lem  8522  infmap2  8619  cfslb2n  8669  sornom  8678  isfin4  8698  fin23lem26  8726  fin23lem27  8729  fin1a2lem11  8811  fin1a2lem12  8812  hsmex  8833  domtriomlem  8843  dominf  8846  zorn2lem2  8898  zorn2lem7  8903  zorn2g  8904  axdclem  8920  axdc  8922  fodomg  8924  brdom7disj  8930  brdom6disj  8931  cardmin  8960  ficard  8961  alephval2  8968  dominfac  8969  cfpwsdom  8980  gchi  9023  fpwwe2lem12  9040  fpwwe2lem13  9041  canthp1lem1  9051  canthp1lem2  9052  pwfseqlem4a  9060  pwfseqlem4  9061  elina  9086  winainflem  9092  eltskg  9149  rankcf  9176  indpi  9306  nqereu  9328  nsmallnq  9376  ltbtwnnq  9377  ltrnq  9378  prcdnq  9392  genpcd  9405  genpnmax  9406  ltaddpr2  9434  ltexprlem4  9438  prlem936  9446  reclem2pr  9447  reclem3pr  9448  supexpr  9453  ltsosr  9492  ltasr  9498  recexsrlem  9501  mulgt0sr  9503  map2psrpr  9508  supsrlem  9509  axpre-lttri  9563  axpre-lttrn  9564  axpre-ltadd  9565  axpre-mulgt0  9566  axpre-sup  9567  ltletr  9697  letr  9699  ltne  9702  eqle  9708  dedekind  9765  dedekindle  9766  ltordlem  10103  elimgt0  10403  elimge0  10404  squeeze0  10473  fimaxre2  10516  lbreu  10518  lble  10520  sup2  10524  infm3  10527  suprlub  10530  supmul1  10533  supmullem1  10534  supmullem2  10535  supmul  10536  infmrcl  10547  infmrgelb  10548  nn2ge  10586  nnge1  10587  nnsub  10599  nominpos  10800  nnunb  10816  elnnnn0b  10865  nn0sub  10871  nn0ge2m1nn  10886  peano2uz2  10975  peano5uzi  10976  dfuzi  10978  uzind  10979  uzind3  10981  uzindOLD  10982  uzind3OLD  10983  eluz1  11114  uzind4  11168  uzwo  11173  uzwoOLD  11174  nnwof  11177  indstr2  11189  ublbneg  11195  zsupss  11200  uzsupss  11203  uzwo3  11206  zmin  11207  zmax  11208  zbtwnre  11209  rebtwnz  11210  rpnnen1lem1  11237  rpnnen1lem2  11238  rpnnen1lem3  11239  rpnnen1lem4  11240  rpnnen1lem5  11241  reexALT  11243  elrp  11251  mnfltxr  11365  nn0pnfge0  11370  xrltnsym  11372  xrlttri  11374  xrlttr  11375  xrltletr  11389  xrletr  11390  ngtmnft  11397  xrltmin  11412  xrlemin  11414  ifle  11425  z2ge  11426  qbtwnre  11427  qbtwnxr  11428  qextlt  11431  qextle  11432  xltnegi  11444  xmullem2  11486  xmulasslem2  11503  xmulasslem  11506  xlemul1a  11509  xrsupexmnf  11525  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  supxrpnf  11539  supxrunb1  11540  supxrunb2  11541  ixxval  11566  elixx1  11567  elioo2  11599  iccid  11603  icc0  11606  iccsupr  11646  repos  11650  supicc  11697  supiccub  11698  supicclub  11699  fzval  11703  elfz1  11706  fzm1  11787  flval  11931  flval2  11950  flval3  11951  dfceil2  11968  uzsup  11990  modid2  12023  fsequb  12085  ssnn0fi  12094  rabssnn0fi  12095  suppssfz  12100  serge0  12161  expge0  12202  expge1  12203  facdiv  12365  facwordi  12367  hashkf  12407  hashnnn0genn0  12416  hashv01gt1  12418  hashneq0  12434  hashdom  12447  hashnn0n0nn  12458  hashss  12474  hashgt12el  12481  hashgt12el2  12482  hashge2el2dif  12521  brfi1uzind  12532  wrdlen1  12579  fstwrdne0  12581  wrdeqswrdlsw  12674  2swrdeqwrdeq  12678  2swrd1eqwrdeq  12679  ccats1swrdeq  12694  ccats1swrdeqrex  12704  swrdccatin12lem3  12715  2swrd2eqwrdeq  12891  shftfib  12905  shftfn  12906  2shfti  12913  sqrlem3  13078  resqrex  13084  cau3lem  13187  caubnd2  13190  caubnd  13191  sqreu  13193  limsuple  13301  limsupval2  13303  rlim2  13319  climi  13333  rlimi  13336  ello12r  13340  ello1mpt  13344  ello1d  13346  lo1bdd2  13347  lo1bddrp  13348  elo12r  13351  o1lo1  13360  rlimclim1  13368  rlimdm  13374  climeu  13378  climmo  13380  2clim  13395  o1co  13409  o1compt  13410  addcn2  13416  mulcn2  13418  reccn2  13419  cn1lem  13420  rlimo1  13439  lo1add  13449  lo1mul  13450  climsup  13492  caucvgrlem  13495  caucvgb  13502  summo  13539  zsum  13540  fsum  13542  o1fsum  13627  climcnds  13663  supcvg  13667  ntrivcvgn0  13707  ntrivcvgmullem  13710  prodmo  13743  zprod  13744  fprod  13748  fprodntriv  13749  rpnnen2lem4  13951  rpnnen  13960  ruclem2  13965  ruclem12  13974  sqrt2irr  13982  dvdsabsb  14003  0dvds  14004  dvdsle  14031  alzdvds  14036  dvdsext  14037  fzo0dvdseq  14039  divalglem10  14060  bitsinv1lem  14091  sadadd3  14111  bitsuz  14124  gcdval  14146  gcdcllem1  14149  gcdcllem2  14150  gcddvds  14153  bezoutlem4  14179  dvdsgcd  14181  dvdssq  14198  isprm  14219  isprm2lem  14224  dvdsprm  14240  coprmdvds2  14244  isprm6  14250  exprmfct  14251  maxprmfct  14254  prmexpb  14258  prmfac1  14259  rpexp  14261  iserodd  14359  pceu  14370  pczpre  14371  pcdiv  14376  pcdvdsb  14392  pcmpt  14411  pcmptdvds  14413  prmpwdvds  14422  unbenlem  14426  infpnlem2  14429  infpn2  14431  prmreclem1  14434  prmreclem2  14435  prmreclem3  14436  prmreclem5  14438  prmreclem6  14439  vdwlem9  14507  vdwlem10  14508  vdwlem13  14511  ramz  14543  imasleval  14938  mreexexlem3d  15043  mreexexlem4d  15044  mreexexd  15045  prslem  15560  drsdirfi  15567  posi  15579  posasymb  15582  pleval2  15595  plttr  15600  pltletr  15601  pospo  15603  lubprop  15616  lublecllem  15618  glbprop  15629  glble  15630  joinlem  15641  joinle  15644  meetval2lem  15652  meetlem  15655  isglbd  15747  lubl  15750  lubun  15753  pospropd  15764  poslubmo  15776  posglbmo  15777  poslubd  15778  tsrlin  15849  tsrlemax  15850  letsr  15857  eqgen  16254  odeq  16574  odmulg  16578  pgpssslw  16634  sylow2alem2  16638  sylow2blem3  16642  efgval2  16742  efgsfo  16757  efgred  16766  efgredeu  16770  efgcpbllemb  16773  gexex  16859  cyggex2  16899  gsummptnn0fz  17014  gsummptnn0fzfv  17016  pgpfaclem1  17132  pgpfaclem2  17133  pgpfaclem3  17134  ablfaclem2  17137  ablfaclem3  17138  lidldvgen  17903  0ringnnzr  17917  psrass1lem  18029  psrmulval  18039  mplmonmul  18126  opsrtoslem2  18149  coe1mul2  18310  coe1tmmul2fv  18319  coe1pwmulfv  18321  gsummoncoe1  18346  zndvds  18588  znleval  18593  islinds  18844  pmatcoe1fsupp  19202  mp2pm2mplem4  19310  fvmptnn04ifa  19351  fvmptnn04ifd  19354  chfacffsupp  19357  chfacfscmul0  19359  chfacfpmmul0  19363  cpmadumatpoly  19384  cayleyhamilton  19391  cayleyhamiltonALT  19392  ordtbaslem  19689  ordtbas2  19692  ordtopn1  19695  mnfnei  19722  ordtt1  19880  ordthauslem  19884  ordthmeolem  20302  trust  20732  ucncn  20788  imasdsf1olem  20876  comet  21016  stdbdxmet  21018  stdbdmet  21019  stdbdmopn  21021  metcnpi  21047  metcnpi2  21048  metcnpi3  21049  ngptgp  21150  nlmvscnlem1  21195  nrginvrcnlem  21199  nmogelb  21223  nmolb  21224  nghmcn  21252  xrsxmet  21314  icccmplem2  21328  icccmplem3  21329  reconnlem2  21332  xrge0tsms  21339  xmetdcn2  21342  metdsf  21352  metdsge  21353  metdscn  21360  metnrmlem1a  21362  addcnlem  21368  cncfi  21398  elcncf1di  21399  iccpnfhmeo  21445  xrhmeo  21446  cnllycmp  21456  evth  21459  ipcnlem1  21685  lmmcvg  21700  cfili  21707  cncmet  21761  minveclem1  21839  minveclem3b  21843  minveclem6  21849  pmltpclem1  21860  pmltpc  21862  ivthlem2  21864  ivthlem3  21865  cniccbdd  21873  ovolmge0  21888  ovolgelb  21891  ovolctb  21901  ovolunlem1  21908  ovoliunlem1  21913  ovoliun  21916  ovoliun2  21917  ovolshftlem1  21920  ovolscalem1  21924  ovolicc2lem3  21930  ovolicc2lem5  21932  ovolicc2  21933  voliunlem3  21962  ioombl1lem1  21968  ioombl1lem4  21971  uniioombllem2  21992  uniioombllem6  21997  volcn  22015  ismbfd  22047  mbfsup  22071  mbfinf  22072  mbflimsup  22073  itg1ge0  22093  itg1climres  22121  mbfi1fseqlem5  22126  itg2val  22135  itg2const  22147  itg2const2  22148  itg2seq  22149  itg2monolem1  22157  itg2i1fseq  22162  itg2i1fseq2  22163  itg2addlem  22165  itg2cnlem1  22168  itg2cnlem2  22169  itg2cn  22170  isibl  22172  ditgeq2  22253  dveflem  22380  dvferm1lem  22385  rolle  22391  c1lip1  22398  lhop1  22415  dvfsumlem2  22428  dvfsumlem4  22430  dvfsumrlim  22432  dvfsum2  22435  mdegmullem  22478  deg1leb  22495  deg1lt  22498  dvdsq1p  22561  plyeq0lem  22607  dgrco  22672  plydivex  22693  quotcan  22705  aannenlem1  22724  aannenlem2  22725  ulmi  22781  ulmcaulem  22789  ulmcau  22790  ulmbdd  22793  ulmdvlem3  22797  mtestbdd  22800  iblulm  22802  psercnlem1  22820  psercn  22821  abelthlem8  22834  sinhalfpilem  22856  logltb  22984  cxple2  23078  cxpcn3lem  23121  isosctrlem1  23152  leibpilem2  23272  cxploglim  23307  scvxcvx  23315  emcllem6  23330  ftalem3  23348  vmaval  23387  isppw2  23389  muval  23406  fsumdvdscom  23461  dvdsflf1o  23463  dvdsflsumcom  23464  musum  23467  muinv  23469  ppiublem1  23477  chtub  23487  logfac2  23492  bpos1lem  23557  bposlem9  23567  lgsdir  23605  lgsne0  23608  lgsqr  23621  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  2sqlem6  23644  2sqlem8  23647  2sqlem10  23649  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  dchrvmasumiflem1  23686  dchrisum0fval  23690  dchrisum0ff  23692  dchrisum0flblem2  23694  logsqvma2  23728  pntrsumbnd2  23752  pntrlog2bndlem1  23762  pntpbnd1  23771  pntpbnd2  23772  pntibndlem2  23776  pntibndlem3  23777  pntibnd  23778  pntlemi  23789  pntlem3  23794  pntlemp  23795  pntleml  23796  pnt3  23797  tgldimor  23893  lnopp2hpgb  24132  axcontlem10  24276  uhgra0v  24310  usgra0v  24371  usgra1v  24390  cusgraexg  24469  sizeusglecusg  24486  usgramaxsize  24487  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv  24667  wwlknred  24723  wwlkextwrd  24728  wwlkextfun  24729  wwlkextinj  24730  wwlkextproplem2  24742  wwlkextproplem3  24743  clwlkisclwwlklem1  24787  clwwlkf1  24796  clwwlkext2edg  24802  wwlkext2clwwlk  24803  wwlksubclwwlk  24804  clwlkfclwwlk  24844  clwlkfoclwwlk  24845  rusgranumwlks  24956  isfrgra  24990  vdgfrgragt2  25027  frgrawopreglem2  25045  clwwlkextfrlem1  25076  numclwwlkovf2ex  25086  friendshipgt3  25121  gxval  25260  vacn  25604  nmcvcn  25605  smcnlem  25607  nmobndi  25690  blocni  25720  ubthlem1  25786  ubthlem2  25787  ubthlem3  25788  minvecolem1  25790  minvecolem5  25797  minvecolem6  25798  htthlem  25834  norm3lemt  26069  hcaucvg  26103  hlimconvi  26108  hlim2  26109  chlimi  26152  hlimreui  26157  occl  26222  cmbr3  26526  cmcm  26532  cmcm3  26533  lecm  26535  cnopc  26832  cnfnc  26849  0cnop  26898  0cnfn  26899  idcnop  26900  nmopun  26933  nmcexi  26945  lnconi  26952  branmfn  27024  opsqrlem1  27059  pjnmopi  27067  pjnormssi  27087  stge1i  27157  strlem5  27174  hstrlem5  27182  mddmd2  27228  csmdsymi  27253  cvmd  27255  ela  27258  cvbr4i  27286  chirredlem3  27311  chirredlem4  27312  chirred  27314  atmd  27318  mdsym  27331  mddmdin0i  27350  cdj1i  27352  cdj3i  27360  fmptcof2  27502  isoun  27520  xrge0infss  27580  ishashinf  27606  tleile  27649  toslublem  27655  tosglblem  27657  omndadd  27696  sgnsval  27718  xrnarchi  27728  archirng  27732  archiexdiv  27734  archiabllem1a  27735  archiabllem2a  27738  archiabl  27742  xrge0tsmsd  27775  orngmul  27793  isarchiofld  27807  crefi  27850  pcmplfin  27863  ordtconlem1  27906  rge0scvg  27931  qqhcn  27972  qqhucn  27973  esumcst  28071  esumpinfval  28079  esumpcvgval  28084  esumcvg  28092  oddpwdc  28293  eulerpartlems  28299  eulerpartlemf  28309  eulerpartlemt  28310  eulerpartlemr  28313  eulerpartlemgvv  28315  eulerpartlemn  28320  dstfrvunirn  28413  ballotlemfcc  28432  sgnmulsgp  28489  signslema  28519  lgamgulmlem4  28574  lgamgulmlem5  28575  lgambdd  28579  subfacp1lem1  28623  relexpindlem  29062  relexpind  29063  rtrclreclem.trans  29069  dfpo2  29184  fundmpss  29196  funbreq  29201  dfpred3g  29255  predbrg  29266  poseq  29333  wzel  29380  wsuclem  29381  wsuclb  29384  nodenselem4  29444  nodenselem5  29445  nodense  29449  nocvxminlem  29450  nobndup  29460  nofulllem5  29466  brtxp  29530  brtxp2  29531  brpprod3a  29536  elfix  29553  sscoid  29563  elfuns  29565  fnsingle  29569  brimageg  29577  fnimage  29579  brdomaing  29585  brrangeg  29586  funpartlem  29592  fvtransport  29682  fin2so  30040  supaddc  30041  supadd  30042  heicant  30049  mblfinlem1  30051  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  itg2addnclem  30066  itg2addnc  30069  itg2gt0cn  30070  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  trer  30134  elicc3  30135  finminlem  30136  nn0prpwlem  30140  nn0prpw  30141  fnessref  30175  refssfne  30176  fnemeet2  30185  filnetlem3  30198  frinfm  30226  fdc1  30239  nninfnub  30244  equivbnd  30286  heibor1lem  30305  heiborlem8  30314  iccbnd  30336  lzenom  30703  fphpdo  30751  rencldnfilem  30754  irrapxlem5  30762  irrapxlem6  30763  pellexlem3  30767  pellqrex  30815  pellfundre  30817  pellfundge  30818  pellfundlb  30820  pellfundglb  30821  monotoddzz  30879  oddcomabszz  30880  zindbi  30882  jm2.22  30937  jm2.23  30938  rpnnen3  30974  ttac  30978  fnwe2lem2  30997  aomclem8  31007  hbtlem1  31072  hbtlem5  31077  lcmcllem  31202  dvdslcm  31204  lcmledvds  31205  lcmgcdlem  31212  lcmdvds  31214  nzss  31222  ubelsupr  31395  climinf  31612  mullimc  31622  limcdm0  31624  mullimcf  31629  constlimc  31630  idlimc  31632  limsupre  31647  limcleqr  31650  addlimc  31654  0ellimcdiv  31655  limclner  31657  dvdivbd  31720  dvbdfbdioo  31727  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnxpaek  31739  stoweidlem14  31796  stoweidlem29  31811  stoweidlem31  31813  stoweidlem34  31816  stoweidlem49  31831  wallispilem3  31849  stirlinglem13  31868  stirlinglem14  31869  fourierdlem16  31905  fourierdlem20  31909  fourierdlem21  31910  fourierdlem22  31911  fourierdlem25  31914  fourierdlem39  31928  fourierdlem41  31930  fourierdlem42  31931  fourierdlem51  31940  fourierdlem54  31943  fourierdlem64  31953  fourierdlem77  31966  fourierdlem83  31972  fourierdlem87  31976  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fouriersw  32014  etransclem48  32065  rlimdmafv  32262  assintopval  32529  ply1mulgsumlem2  32987  ldepsnlinc  33109  bnj1185  33852  bnj602  33973  bnj1228  34067  bj-seex  34491  oposlem  34907  lub0N  34914  glb0N  34918  omllaw  34968  cvrval  34994  cvrnbtwn  34996  cvrnbtwn2  35000  cvrnbtwn3  35001  cvrcon3b  35002  cvrnbtwn4  35004  cvrcmp  35008  isat  35011  atnlt  35038  atlex  35041  cvlexch1  35053  cvlexchb1  35055  cvlatexch1  35061  glbconN  35101  2llnne2N  35132  cvratlem  35145  cvrat4  35167  ps-1  35201  3at  35214  islln  35230  llncmp  35246  llnnlt  35247  islpln  35254  islpln5  35259  lvolex3N  35262  lplncmp  35286  lplnexllnN  35288  lplnnlt  35289  islvol  35297  lvoli3  35301  islvol5  35303  lvolcmp  35341  lvolnltN  35342  dalem-cly  35395  dalem44  35440  pmapval  35481  pmapglbx  35493  lncvrelatN  35505  lncmp  35507  cdlemblem  35517  llnexchb2  35593  lautle  35808  lautcvr  35816  ldilset  35833  ltrnset  35842  trlset  35886  cdlemc4  35919  cdleme11dN  35987  cdleme20k  36045  cdleme21ct  36055  cdleme22b  36067  tendoex  36701  diafval  36758  diaval  36759  dicfval  36902  dihfval  36958  dihglblem2N  37021  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