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

Theorem breq1 4175
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 3944 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2470 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 4173 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 4173 . 2  |-  ( B R C  <->  <. B ,  C >.  e.  R )
52, 3, 43bitr4g 280 1  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1721   <.cop 3777   class class class wbr 4172
This theorem is referenced by:  breq12  4177  breq1i  4179  breq1d  4182  nbrne2  4190  brab1  4217  pocl  4470  swopolem  4472  swopo  4473  solin  4486  sotrieq  4490  sotr2  4492  isso2i  4495  somo  4497  frirr  4519  fr2nr  4520  wereu2  4539  fr3nr  4719  dfwe2  4721  vtoclr  4881  frsn  4907  brcog  4998  brcogw  5000  opelcnvg  5011  dfdmf  5023  eldmg  5024  dfrnf  5067  dfres2  5152  imasng  5185  asymref2  5210  sotri2  5222  somin1  5229  coi1  5344  dffun6f  5427  funmo  5429  fun11  5475  fveq2  5687  nfunsn  5720  dffv2  5755  dff3  5841  f1ompt  5850  fmptco  5860  dff13  5963  foeqcnvco  5986  isorel  6005  soisores  6006  soisoi  6007  isocnv  6009  isotr  6015  isomin  6016  isoini  6017  isopolem  6024  isosolem  6026  f1oiso  6030  f1oiso2  6031  f1oweALT  6033  weniso  6034  caovordig  6211  caovordg  6213  caovord3d  6216  caovord  6217  caovord3  6219  caofrss  6296  caoftrn  6298  frxp  6415  poxp  6417  fnse  6422  brtpos2  6444  rntpos  6451  tpostpos  6458  fvopab5  6493  ertr  6879  ecopovsym  6965  ecopovtrn  6966  th3qlem2  6970  isfi  7090  en0  7129  en1  7133  endisj  7154  xpcomco  7157  sbth  7186  2pwne  7222  disjenex  7224  ssenen  7240  nneneq  7249  php  7250  sdom1  7267  isinf  7281  fineqvlem  7282  pssnn  7286  enp1i  7302  findcard  7306  findcard2  7307  findcard3  7309  frfi  7311  fiint  7342  marypha1lem  7396  supmo  7413  eqsup  7417  supub  7420  suplub  7421  supmaxlem  7425  suppr  7429  supisolem  7431  supisoex  7432  ordtypecbv  7442  ordtypelem3  7445  ordtypelem6  7448  ordtypelem7  7449  ordtypelem9  7451  ordtypelem10  7452  hartogslem1  7467  hartogs  7469  wemaplem1  7471  wemaplem2  7472  card2on  7478  card2inf  7479  elharval  7487  brwdom2  7497  wdomtr  7499  cantnfp1lem2  7591  cantnflem1  7601  wemapwe  7610  r111  7657  kardex  7774  karden  7775  isnumi  7789  tskwe  7793  cardid2  7796  cardonle  7800  cardne  7808  iscard2  7819  infxpenlem  7851  fodomfi2  7897  wdomfil  7898  wdomnumr  7901  alephsuc2  7917  infenaleph  7928  iunfictbso  7951  infpss  8053  cff1  8094  cfslb2n  8104  sornom  8113  fin4i  8134  isfin6  8136  isfin7  8137  isfin1-3  8222  fin1a2lem9  8244  fin1a2lem11  8246  hsmexlem4  8265  axcc2lem  8272  axcc4dom  8277  domtriomlem  8278  numthcor  8330  zorn2lem2  8333  zorn2lem3  8334  zorn2lem7  8338  zorn2g  8339  axdclem  8355  axdc  8357  brdom7disj  8365  brdom6disj  8366  uniimadom  8375  ondomon  8394  alephval2  8403  alephreg  8413  pwcfsdom  8414  elgch  8453  gchi  8455  fpwwe2lem12  8472  fpwwe2lem13  8473  pwfseqlem4  8493  winainflem  8524  winalim2  8527  tsken  8585  0tsk  8586  inar1  8606  tskord  8611  tskuni  8614  grudomon  8648  pinq  8760  nqereu  8762  enqeq  8767  ltbtwnnq  8811  ltrnq  8812  prcdnq  8826  prnmax  8828  genpnmax  8840  nqpr  8847  1idpr  8862  reclem2pr  8881  reclem3pr  8882  reclem4pr  8883  recexpr  8884  supexpr  8887  ltsosr  8925  1ne0sr  8927  ltasr  8931  supsrlem  8942  axpre-lttri  8996  axpre-lttrn  8997  axpre-ltadd  8998  axpre-sup  9000  lelttr  9121  ltordlem  9508  lt0ne0d  9548  fimaxre3  9913  lbreu  9914  lble  9916  sup2  9920  infm3  9923  suprleub  9928  supmul1  9929  supmullem1  9930  supmul  9932  nnsub  9994  nominpos  10160  nnunb  10173  arch  10174  nn0sub  10226  nn0n0n1ge2b  10237  zextle  10299  peano5uzti  10315  fzind  10324  btwnz  10328  uzval  10446  uzwo  10495  uzwoOLD  10496  nnwof  10499  uzinfmi  10511  ublbneg  10516  lbzbi  10520  zsupss  10521  uzsupss  10524  uzwo3  10525  zmax  10527  rebtwnz  10529  rpnnen1lem3  10558  xrltnsym  10686  xrlttri  10688  xrlttr  10689  xrlelttr  10702  nltpnft  10710  xrmaxlt  10725  xrmaxle  10727  qbtwnre  10741  qbtwnxr  10742  xltnegi  10758  xsubge0  10796  xlesubadd  10798  xmullem2  10800  xlemul1a  10823  xrinfmexpnf  10840  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  supxrunb1  10854  supxrunb2  10855  ixxval  10880  elixx1  10881  elioo2  10913  iccid  10917  icc0  10920  fzval  11001  elfz1  11004  elfznelfzo  11147  elfznelfzob  11148  flval  11158  fllelt  11161  flval2  11176  flval3  11177  flbi  11178  modid2  11226  fsequb2  11270  seqf1olem2  11318  sqlecan  11442  faclbnd4lem1  11539  sqrlem6  12008  01sqrex  12010  abslt  12073  absle  12074  rexanre  12105  rexico  12112  limsupgle  12226  limsupgre  12230  limsupbnd2  12232  rlim2lt  12246  rlim3  12247  ello12r  12266  ello1d  12272  elo12r  12277  rlimconst  12293  climshft  12325  rlimcn2  12339  o1rlimmul  12367  lo1le  12400  climsup  12418  caucvgrlem  12421  isumless  12580  divrcnv  12587  cvgrat  12615  rpnnen2lem10  12778  ruclem1  12785  ruclem2  12786  ruclem11  12794  ruclem12  12795  sqr2irr  12803  absdvdsb  12823  dvdsle  12850  dvdseq  12852  dvdsext  12855  divalglem8  12875  divalglem9  12876  divalglem10  12877  divalgmod  12881  ndvdssub  12882  sadcaddlem  12924  gcdcllem1  12966  gcdcllem2  12967  gcdcllem3  12968  gcdeq  13007  dvdssq  13015  nn0seqcvgd  13016  algcvgblem  13023  1nprm  13039  1idssfct  13040  isprm2lem  13041  isprm2  13042  dvdsprime  13047  nprm  13048  3prm  13051  dvdsprm  13054  coprm  13055  exprmfct  13065  isprm5  13067  maxprmfct  13068  eulerthlem2  13126  odzval  13132  pythagtriplem4  13148  pc2dvds  13207  pcprmpw2  13210  pcprmpw  13211  prmpwdvds  13227  pockthg  13229  unbenlem  13231  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  1arith  13250  vdwlem6  13309  vdwlem11  13314  vdwlem13  13316  ramtlecl  13323  ramub  13336  rami  13338  ramubcl  13341  0ram  13343  ram0  13345  prmlem0  13383  prmlem1a  13384  imasaddfnlem  13708  imasvscafn  13717  imasleval  13721  prslem  14343  drsdir  14347  drsdirfi  14350  isdrs2  14351  posi  14362  posasymb  14364  pltval3  14379  plelttr  14384  pospo  14385  lubprop  14392  luble  14393  lubid  14394  glbprop  14397  joinval2  14401  joinlem  14402  meetlem  14409  meetle  14412  latnlej  14452  isglbd  14499  lubub  14501  lubun  14505  clatleglb  14508  pospropd  14516  poslubmo  14528  poslubd  14529  tsrlin  14606  spwmo  14613  spwpr2  14615  spwpr4  14618  letsr  14627  dirge  14637  mndodcongi  15136  odeq  15143  odmulgeq  15148  gexnnod  15177  sylow1lem1  15187  pgpssslw  15203  sylow2a  15208  efgredeu  15339  efgred2  15340  gexex  15423  frgpnabllem2  15440  cyggenod  15449  dprdval  15516  ablfacrplem  15578  ablfac1c  15584  ablfac1eu  15586  ablfaclem3  15600  abvtrivd  15883  psrbagconcl  16393  psrbagconf1o  16394  gsumbagdiaglem  16395  psrmulcllem  16406  psrlidm  16422  psrridm  16423  psrass1  16424  psrcom  16427  mplmonmul  16482  coe1mul2  16617  coe1tmmul  16624  zlpir  16726  prmirredlem  16728  znleval  16790  ordtbas2  17209  ordtopn2  17213  ordtrest2lem  17221  pnfnei  17238  ordtt1  17397  ordthauslem  17401  2ndci  17464  2ndcsb  17465  2ndcredom  17466  2ndc1stc  17467  1stcrest  17469  2ndcctbss  17471  2ndcdisj  17472  2ndcsep  17475  lly1stc  17512  tx1stc  17635  ordthmeolem  17786  ufildom1  17911  xmetrtri2  18339  prdsxmetlem  18351  ssblex  18411  prdsbl  18474  comet  18496  stdbdxmet  18498  stdbdmopn  18501  met1stc  18504  dscmet  18573  metdstri  18834  metdscn  18839  xrhmeo  18924  bndth  18936  evth  18937  lebnumlem3  18941  pcovalg  18990  pco1  18993  pcocn  18995  pcopt  19000  pcopt2  19001  pcoass  19002  nmoleub3  19080  bcthlem5  19234  minveclem4c  19279  minveclem2  19280  minveclem3b  19282  minveclem4  19286  minveclem6  19288  pmltpclem1  19298  pmltpc  19300  ovollb2lem  19337  ovolctb  19339  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem2  19352  ovoliun2  19355  ovolshftlem1  19358  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem3  19368  voliunlem2  19398  voliunlem3  19399  ioombl1lem4  19408  uniioovol  19424  uniioombllem2  19428  uniioombllem3  19430  uniioombllem6  19433  volsup2  19450  ismbfd  19485  mbfsup  19509  mbflimsup  19511  itg1climres  19559  mbfi1fseqlem4  19563  itg2lr  19575  itg2leub  19579  itg2seq  19587  itg2monolem1  19595  itg2monolem3  19597  itg2mono  19598  itg2i1fseq2  19601  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  itg2cn  19608  iblss  19649  itgless  19661  ibladdlem  19664  iblabsr  19674  iblmulc2  19675  itgabs  19679  ditgeq1  19688  dvferm2lem  19823  rolle  19827  dvlip2  19832  c1liplem1  19833  c1lip1  19834  dvfsumlem2  19864  dvfsumlem4  19866  mdegleb  19940  degltlem1  19948  plyco0  20064  plyeq0lem  20082  coeeq2  20114  dgrle  20115  dgradd2  20139  plydiveu  20168  aareccl  20196  aalioulem2  20203  aaliou3lem7  20219  psercnlem1  20294  pilem2  20321  pilem3  20322  logltb  20447  divlogrlim  20479  logcnlem3  20488  cxpaddlelem  20588  rlimcnp  20757  cxplim  20763  cxploglim  20769  scvxcvx  20777  ftalem1  20808  ftalem2  20809  isppw2  20851  vmappw  20852  sgmnncl  20883  sqff1o  20918  dvdsdivcl  20919  fsumdvdsdiaglem  20921  dvdsppwf1o  20924  dvdsflsumcom  20926  musum  20929  muinv  20931  dvdsmulf1o  20932  vmalelog  20942  vmasum  20953  logfac2  20954  perfectlem2  20967  bcmono  21014  bpos1lem  21019  bposlem9  21029  lgsmod  21058  lgsne0  21070  2sqlem6  21106  2sqlem8  21109  2sqlem10  21111  chtppilim  21122  rpvmasumlem  21134  dchrisumlema  21135  dchrisumlem2  21137  dchrvmasumlem1  21142  dchrvmasumiflem1  21148  dchrisum0flblem1  21155  dchrisum0flblem2  21156  dchrisum0  21167  rplogsum  21174  logsqvma  21189  pntpbnd1  21233  pntpbnd2  21234  pntibndlem3  21239  pntlemj  21250  pntlemi  21251  pntlem3  21256  pnt3  21259  ostth3  21285  usgra1v  21362  usgrafisindb0  21375  usgrafisindb1  21376  cusgra1v  21423  1conngra  21615  eupath2  21655  gxnval  21801  rngosn4  21968  rngoueqz  21971  nmoubi  22226  minvecolem2  22330  minvecolem3  22331  minvecolem4c  22334  minvecolem4  22335  minvecolem5  22336  minvecolem6  22337  htthlem  22373  chlimi  22690  chcompl  22698  hsn0elch  22703  cmbr3  23063  cmcm  23069  cmcm3  23070  lecm  23072  nmopub  23364  nmfnleub  23381  nmopun  23470  nmcexi  23482  cnlnadjlem7  23529  pjnmopi  23604  stle0i  23695  stlesi  23697  stm1i  23699  csmdsymi  23790  cvmd  23792  atcveq0  23804  atcv1  23836  atord  23844  atcvat2  23845  chirred  23851  mdsym  23868  mddmdin0i  23887  cdj1i  23889  fmptcof2  24029  isoun  24042  lt2addrd  24068  xlt2addrd  24077  xrofsup  24079  tleile  24142  toslub  24144  tosglb  24145  ofldadd  24191  ofldmul  24192  xrnarchi  24207  xrge0iifiso  24274  rge0scvg  24288  gsumesum  24404  esumfsup  24413  esumpinfval  24416  esumpcvgval  24421  esumcvg  24429  sigaclcu  24453  sigaclci  24468  unelsiga  24470  measvun  24516  voliune  24538  volfiniune  24539  orvcval2  24669  dstfrvel  24684  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemsv  24720  ballotlemsf1o  24724  relexpindlem  25092  rtrclreclem.trans  25099  dedekind  25140  dedekindle  25141  dfdm5  25346  dfrn5  25347  trpredpred  25445  poseq  25467  nodense  25557  nocvxminlem  25558  nobnddown  25569  nofulllem4  25573  nofulllem5  25574  brpprod  25639  brsset  25643  brbigcup  25652  dffix2  25659  elfuns  25668  brimageg  25680  brdomaing  25688  brrangeg  25689  brimg  25690  brapply  25691  brsuccf  25694  funpartlem  25695  brrestrict  25702  dfrdg4  25703  axlowdim2  25803  axlowdim  25804  axcontlem2  25808  axcontlem3  25809  axcontlem4  25810  axcontlem7  25813  axcontlem9  25815  axcontlem10  25816  axcontlem11  25817  axcontlem12  25818  brofs  25843  btwncomim  25851  btwnintr  25857  btwnexch3  25858  btwnexch2  25861  brifs  25881  brcolinear2  25896  colineardim1  25899  brfs  25917  btwnconn1  25939  segcon2  25943  seglerflx  25950  seglemin  25951  btwnsegle  25955  colinbtwnle  25956  broutsideof2  25960  fvray  25979  lineunray  25985  lineelsb2  25986  linerflx1  25987  supaddc  26137  supadd  26138  ltflcei  26140  lxflflp1  26142  mblfinlem  26143  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  ibladdnclem  26160  iblmulc2nc  26169  itgabsnc  26173  bddiblnc  26174  trer  26209  elicc3  26210  finminlem  26211  nn0prpwlem  26215  nn0prpw  26216  indexdom  26326  filbcmb  26332  fdc  26339  prdsbnd  26392  heiborlem3  26412  rrnequiv  26434  prtlem10  26604  lzenom  26718  fphpdo  26768  irrapxlem4  26778  pellexlem6  26787  infmrgelbi  26831  pellfundre  26834  pellfundlb  26837  monotoddzz  26896  zindbi  26899  divalgmodcl  26948  jm2.27  26969  rmydioph  26975  rpnnen3lem  26992  fnwe2lem2  27016  aomclem8  27027  hbtlem5  27200  hbt  27202  pmtrval  27262  pmtrrn  27267  pmtrfrn  27268  phisum  27386  stoweidlem5  27621  stoweidlem20  27636  stoweidlem26  27642  stoweidlem28  27644  stoweidlem29  27645  stoweidlem34  27650  wallispilem3  27683  stirlinglem13  27702  funressnfv  27859  dfdfat2  27862  tz6.12-afv  27904  swrdccat3  28029  swrdccat3b  28031  isfrgra  28094  3vfriswmgra  28109  1to2vfriswmgra  28110  vdfrgra0  28126  vdgfrgra0  28127  sgnval  28232  bnj23  28789  bnj1185  28871  bnj1152  29073  bnj1418  29115  lubunNEW  29456  lsatcveq0  29515  lsatcv1  29531  oposlem  29666  opnlen0  29671  lub0N  29672  glb0N  29676  omllaw  29726  cmtbr4N  29738  cvrval  29752  cvrnbtwn  29754  cvrnbtwn2  29758  cvrnbtwn3  29759  cvrcon3b  29760  cvrnbtwn4  29762  atcvreq0  29797  atnle  29800  atlatmstc  29802  cvlexch1  29811  glbconN  29859  hlsuprexch  29863  exatleN  29886  cvratlem  29903  atcvrj0  29910  atcvrj2b  29914  atlelt  29920  cvrat4  29925  3dim1lem5  29948  3dim2  29950  3dim3  29951  ps-2  29960  llni  29990  llnn0  29998  llnle  30000  lplni  30014  lplni2  30019  lplnle  30022  lplnn0N  30029  llncvrlpln  30040  2llnjN  30049  lvoli  30057  lvoli3  30059  lvoli2  30063  lvoln0N  30073  4at  30095  lplncvrlvol  30098  2lplnj  30102  dalemcea  30142  dalem3  30146  psubspi  30229  linepsubN  30234  elpmap  30240  pmapsub  30250  lnatexN  30261  cdlema1N  30273  cdlemb  30276  elpadd  30281  paddvaln0N  30283  paddasslem5  30306  llnexchb2lem  30350  llnexch2N  30352  islhp  30478  lhpat3  30528  4atexlemex2  30553  4atex  30558  4atex2-0aOLDN  30560  4atex2-0cOLDN  30562  lautle  30566  lautcvr  30574  lauteq  30577  ldilval  30595  ltrnu  30603  trlval2  30645  trlne  30667  cdleme0ex1N  30705  cdleme0nex  30772  cdleme18d  30777  cdlemednuN  30782  cdleme25b  30836  cdleme25cv  30840  cdleme27b  30850  cdleme29b  30857  cdleme31sn  30862  cdleme31fv  30872  cdleme31fv2  30875  cdlemefrs29bpre0  30878  cdlemefr29bpre0N  30888  cdlemefr29clN  30889  cdlemefr32fvaN  30891  cdlemefr32fva1  30892  cdlemefs29pre00N  30894  cdlemefs32sn1aw  30896  cdlemefs29bpre0N  30898  cdlemefs29bpre1N  30899  cdlemefs29cpre1N  30900  cdlemefs29clN  30901  cdlemefs32fvaN  30904  cdlemefs32fva1  30905  cdleme41sn3a  30915  cdleme32fva  30919  cdleme32e  30927  cdleme35f  30936  cdleme40v  30951  cdleme42b  30960  trlord  31051  cdlemg1cex  31070  diaval  31515  diaeldm  31519  diaelrnN  31528  cdlemm10N  31601  dibglbN  31649  dicval  31659  dicfnN  31666  dicvalrelN  31668  dihval  31715  dihlsscpre  31717  dihglblem3N  31778  dihmeetlem2N  31782  djhcvat42  31898
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator