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

Theorem breq1 4240
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 4008 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2508 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 4238 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 4238 . 2  |-  ( B R C  <->  <. B ,  C >.  e.  R )
52, 3, 43bitr4g 281 1  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1727   <.cop 3841   class class class wbr 4237
This theorem is referenced by:  breq12  4242  breq1i  4244  breq1d  4247  nbrne2  4255  brab1  4282  pocl  4539  swopolem  4541  swopo  4542  solin  4555  sotrieq  4559  sotr2  4561  isso2i  4564  somo  4566  frirr  4588  fr2nr  4589  wereu2  4608  fr3nr  4789  dfwe2  4791  vtoclr  4951  frsn  4977  brcog  5068  brcogw  5070  opelcnvg  5081  dfdmf  5093  eldmg  5094  dfrnf  5137  dfres2  5222  imasng  5255  asymref2  5280  sotri2  5292  somin1  5299  coi1  5414  dffun6f  5497  funmo  5499  fun11  5545  fveq2  5757  nfunsn  5790  dffv2  5825  dff3  5911  f1ompt  5920  fmptco  5930  dff13  6033  foeqcnvco  6056  isorel  6075  soisores  6076  soisoi  6077  isocnv  6079  isotr  6085  isomin  6086  isoini  6087  isopolem  6094  isosolem  6096  f1oiso  6100  f1oiso2  6101  f1oweALT  6103  weniso  6104  caovordig  6281  caovordg  6283  caovord3d  6286  caovord  6287  caovord3  6289  caofrss  6366  caoftrn  6368  frxp  6485  poxp  6487  fnse  6492  brtpos2  6514  rntpos  6521  tpostpos  6528  fvopab5  6563  ertr  6949  ecopovsym  7035  ecopovtrn  7036  th3qlem2  7040  isfi  7160  en0  7199  en1  7203  endisj  7224  xpcomco  7227  sbth  7256  2pwne  7292  disjenex  7294  ssenen  7310  nneneq  7319  php  7320  sdom1  7337  isinf  7351  fineqvlem  7352  pssnn  7356  enp1i  7372  findcard  7376  findcard2  7377  findcard3  7379  frfi  7381  fiint  7412  marypha1lem  7467  supmo  7486  eqsup  7490  supub  7493  suplub  7494  supmaxlem  7498  suppr  7502  supisolem  7504  supisoex  7505  ordtypecbv  7515  ordtypelem3  7518  ordtypelem6  7521  ordtypelem7  7522  ordtypelem9  7524  ordtypelem10  7525  hartogslem1  7540  hartogs  7542  wemaplem1  7544  wemaplem2  7545  card2on  7551  card2inf  7552  elharval  7560  brwdom2  7570  wdomtr  7572  cantnfp1lem2  7664  cantnflem1  7674  wemapwe  7683  r111  7730  kardex  7849  karden  7850  isnumi  7864  tskwe  7868  cardid2  7871  cardonle  7875  cardne  7883  iscard2  7894  infxpenlem  7926  fodomfi2  7972  wdomfil  7973  wdomnumr  7976  alephsuc2  7992  infenaleph  8003  iunfictbso  8026  infpss  8128  cff1  8169  cfslb2n  8179  sornom  8188  fin4i  8209  isfin6  8211  isfin7  8212  isfin1-3  8297  fin1a2lem9  8319  fin1a2lem11  8321  hsmexlem4  8340  axcc2lem  8347  axcc4dom  8352  domtriomlem  8353  numthcor  8405  zorn2lem2  8408  zorn2lem3  8409  zorn2lem7  8413  zorn2g  8414  axdclem  8430  axdc  8432  brdom7disj  8440  brdom6disj  8441  uniimadom  8450  ondomon  8469  alephval2  8478  alephreg  8488  pwcfsdom  8489  elgch  8528  gchi  8530  fpwwe2lem12  8547  fpwwe2lem13  8548  pwfseqlem4  8568  winainflem  8599  winalim2  8602  tsken  8660  0tsk  8661  inar1  8681  tskord  8686  tskuni  8689  grudomon  8723  pinq  8835  nqereu  8837  enqeq  8842  ltbtwnnq  8886  ltrnq  8887  prcdnq  8901  prnmax  8903  genpnmax  8915  nqpr  8922  1idpr  8937  reclem2pr  8956  reclem3pr  8957  reclem4pr  8958  recexpr  8959  supexpr  8962  ltsosr  9000  1ne0sr  9002  ltasr  9006  supsrlem  9017  axpre-lttri  9071  axpre-lttrn  9072  axpre-ltadd  9073  axpre-sup  9075  lelttr  9196  ltordlem  9583  lt0ne0d  9623  fimaxre3  9988  lbreu  9989  lble  9991  sup2  9995  infm3  9998  suprleub  10003  supmul1  10004  supmullem1  10005  supmul  10007  nnsub  10069  nominpos  10235  nnunb  10248  arch  10249  nn0sub  10301  nn0n0n1ge2b  10312  zextle  10374  peano5uzti  10390  fzind  10399  btwnz  10403  uzval  10521  uzwo  10570  uzwoOLD  10571  nnwof  10574  uzinfmi  10586  ublbneg  10591  lbzbi  10595  zsupss  10596  uzsupss  10599  uzwo3  10600  zmax  10602  rebtwnz  10604  rpnnen1lem3  10633  xrltnsym  10761  xrlttri  10763  xrlttr  10764  xrlelttr  10777  nltpnft  10785  xrmaxlt  10800  xrmaxle  10802  qbtwnre  10816  qbtwnxr  10817  xltnegi  10833  xsubge0  10871  xlesubadd  10873  xmullem2  10875  xlemul1a  10898  xrinfmexpnf  10915  xrsupsslem  10916  xrinfmsslem  10917  xrub  10921  supxrunb1  10929  supxrunb2  10930  ixxval  10955  elixx1  10956  elioo2  10988  iccid  10992  icc0  10995  fzval  11076  elfz1  11079  elfznelfzo  11223  elfznelfzob  11224  flval  11234  fllelt  11237  flval2  11252  flval3  11253  flbi  11254  modid2  11302  fsequb2  11346  seqf1olem2  11394  sqlecan  11518  faclbnd4lem1  11615  sqrlem6  12084  01sqrex  12086  abslt  12149  absle  12150  rexanre  12181  rexico  12188  limsupgle  12302  limsupgre  12306  limsupbnd2  12308  rlim2lt  12322  rlim3  12323  ello12r  12342  ello1d  12348  elo12r  12353  rlimconst  12369  climshft  12401  rlimcn2  12415  o1rlimmul  12443  lo1le  12476  climsup  12494  caucvgrlem  12497  isumless  12656  divrcnv  12663  cvgrat  12691  rpnnen2lem10  12854  ruclem1  12861  ruclem2  12862  ruclem11  12870  ruclem12  12871  sqr2irr  12879  absdvdsb  12899  dvdsle  12926  dvdseq  12928  dvdsext  12931  divalglem8  12951  divalglem9  12952  divalglem10  12953  divalgmod  12957  ndvdssub  12958  sadcaddlem  13000  gcdcllem1  13042  gcdcllem2  13043  gcdcllem3  13044  gcdeq  13083  dvdssq  13091  nn0seqcvgd  13092  algcvgblem  13099  1nprm  13115  1idssfct  13116  isprm2lem  13117  isprm2  13118  dvdsprime  13123  nprm  13124  3prm  13127  dvdsprm  13130  coprm  13131  exprmfct  13141  isprm5  13143  maxprmfct  13144  eulerthlem2  13202  odzval  13208  pythagtriplem4  13224  pc2dvds  13283  pcprmpw2  13286  pcprmpw  13287  prmpwdvds  13303  pockthg  13305  unbenlem  13307  prmreclem4  13318  prmreclem5  13319  prmreclem6  13320  1arith  13326  vdwlem6  13385  vdwlem11  13390  vdwlem13  13392  ramtlecl  13399  ramub  13412  rami  13414  ramubcl  13417  0ram  13419  ram0  13421  prmlem0  13459  prmlem1a  13460  imasaddfnlem  13784  imasvscafn  13793  imasleval  13797  prslem  14419  drsdir  14423  drsdirfi  14426  isdrs2  14427  posi  14438  posasymb  14440  pltval3  14455  plelttr  14460  pospo  14461  lubprop  14468  luble  14469  lubid  14470  glbprop  14473  joinval2  14477  joinlem  14478  meetlem  14485  meetle  14488  latnlej  14528  isglbd  14575  lubub  14577  lubun  14581  clatleglb  14584  pospropd  14592  poslubmo  14604  poslubd  14605  tsrlin  14682  spwmo  14689  spwpr2  14691  spwpr4  14694  letsr  14703  dirge  14713  mndodcongi  15212  odeq  15219  odmulgeq  15224  gexnnod  15253  sylow1lem1  15263  pgpssslw  15279  sylow2a  15284  efgredeu  15415  efgred2  15416  gexex  15499  frgpnabllem2  15516  cyggenod  15525  dprdval  15592  ablfacrplem  15654  ablfac1c  15660  ablfac1eu  15662  ablfaclem3  15676  abvtrivd  15959  psrbagconcl  16469  psrbagconf1o  16470  gsumbagdiaglem  16471  psrmulcllem  16482  psrlidm  16498  psrridm  16499  psrass1  16500  psrcom  16503  mplmonmul  16558  coe1mul2  16693  coe1tmmul  16700  zlpir  16802  prmirredlem  16804  znleval  16866  ordtbas2  17286  ordtopn2  17290  ordtrest2lem  17298  pnfnei  17315  ordtt1  17474  ordthauslem  17478  2ndci  17542  2ndcsb  17543  2ndcredom  17544  2ndc1stc  17545  1stcrest  17547  2ndcctbss  17549  2ndcdisj  17550  2ndcsep  17553  lly1stc  17590  tx1stc  17713  ordthmeolem  17864  ufildom1  17989  xmetrtri2  18417  prdsxmetlem  18429  ssblex  18489  prdsbl  18552  comet  18574  stdbdxmet  18576  stdbdmopn  18579  met1stc  18582  dscmet  18651  metdstri  18912  metdscn  18917  xrhmeo  19002  bndth  19014  evth  19015  lebnumlem3  19019  pcovalg  19068  pco1  19071  pcocn  19073  pcopt  19078  pcopt2  19079  pcoass  19080  nmoleub3  19158  bcthlem5  19312  minveclem4c  19357  minveclem2  19358  minveclem3b  19360  minveclem4  19364  minveclem6  19366  pmltpclem1  19376  pmltpc  19378  ovollb2lem  19415  ovolctb  19417  ovolunlem1  19424  ovoliunlem1  19429  ovoliunlem2  19430  ovoliun2  19433  ovolshftlem1  19436  ovolscalem1  19440  ovolicc1  19443  ovolicc2lem3  19446  voliunlem2  19476  voliunlem3  19477  ioombl1lem4  19486  uniioovol  19502  uniioombllem2  19506  uniioombllem3  19508  uniioombllem6  19511  volsup2  19528  ismbfd  19561  mbfsup  19585  mbflimsup  19587  itg1climres  19635  mbfi1fseqlem4  19639  itg2lr  19651  itg2leub  19655  itg2seq  19663  itg2monolem1  19671  itg2monolem3  19673  itg2mono  19674  itg2i1fseq2  19677  itg2gt0  19681  itg2cnlem1  19682  itg2cnlem2  19683  itg2cn  19684  iblss  19725  itgless  19737  ibladdlem  19740  iblabsr  19750  iblmulc2  19751  itgabs  19755  ditgeq1  19766  dvferm2lem  19901  rolle  19905  dvlip2  19910  c1liplem1  19911  c1lip1  19912  dvfsumlem2  19942  dvfsumlem4  19944  mdegleb  20018  degltlem1  20026  plyco0  20142  plyeq0lem  20160  coeeq2  20192  dgrle  20193  dgradd2  20217  plydiveu  20246  aareccl  20274  aalioulem2  20281  aaliou3lem7  20297  psercnlem1  20372  pilem2  20399  pilem3  20400  logltb  20525  divlogrlim  20557  logcnlem3  20566  cxpaddlelem  20666  rlimcnp  20835  cxplim  20841  cxploglim  20847  scvxcvx  20855  ftalem1  20886  ftalem2  20887  isppw2  20929  vmappw  20930  sgmnncl  20961  sqff1o  20996  dvdsdivcl  20997  fsumdvdsdiaglem  20999  dvdsppwf1o  21002  dvdsflsumcom  21004  musum  21007  muinv  21009  dvdsmulf1o  21010  vmalelog  21020  vmasum  21031  logfac2  21032  perfectlem2  21045  bcmono  21092  bpos1lem  21097  bposlem9  21107  lgsmod  21136  lgsne0  21148  2sqlem6  21184  2sqlem8  21187  2sqlem10  21189  chtppilim  21200  rpvmasumlem  21212  dchrisumlema  21213  dchrisumlem2  21215  dchrvmasumlem1  21220  dchrvmasumiflem1  21226  dchrisum0flblem1  21233  dchrisum0flblem2  21234  dchrisum0  21245  rplogsum  21252  logsqvma  21267  pntpbnd1  21311  pntpbnd2  21312  pntibndlem3  21317  pntlemj  21328  pntlemi  21329  pntlem3  21334  pnt3  21337  ostth3  21363  usgra1v  21440  usgrafisindb0  21453  usgrafisindb1  21454  cusgra1v  21501  1conngra  21693  eupath2  21733  gxnval  21879  rngosn4  22046  rngoueqz  22049  nmoubi  22304  minvecolem2  22408  minvecolem3  22409  minvecolem4c  22412  minvecolem4  22413  minvecolem5  22414  minvecolem6  22415  htthlem  22451  chlimi  22768  chcompl  22776  hsn0elch  22781  cmbr3  23141  cmcm  23147  cmcm3  23148  lecm  23150  nmopub  23442  nmfnleub  23459  nmopun  23548  nmcexi  23560  cnlnadjlem7  23607  pjnmopi  23682  stle0i  23773  stlesi  23775  stm1i  23777  csmdsymi  23868  cvmd  23870  atcveq0  23882  atcv1  23914  atord  23922  atcvat2  23923  chirred  23929  mdsym  23946  mddmdin0i  23965  cdj1i  23967  fmptcof2  24107  isoun  24120  lt2addrd  24146  xlt2addrd  24155  xrofsup  24157  tleile  24220  toslub  24222  tosglb  24223  ofldadd  24269  ofldmul  24270  xrnarchi  24285  xrge0iifiso  24352  rge0scvg  24366  gsumesum  24482  esumfsup  24491  esumpinfval  24494  esumpcvgval  24499  esumcvg  24507  sigaclcu  24531  sigaclci  24546  unelsiga  24548  measvun  24594  voliune  24616  volfiniune  24617  orvcval2  24747  dstfrvel  24762  ballotlemfc0  24781  ballotlemfcc  24782  ballotlemsv  24798  ballotlemsf1o  24802  relexpindlem  25170  rtrclreclem.trans  25177  dedekind  25218  dedekindle  25219  dfdm5  25431  dfrn5  25432  trpredpred  25537  poseq  25559  wsuclem  25607  nodense  25675  nocvxminlem  25676  nobnddown  25687  nofulllem4  25691  nofulllem5  25692  brpprod  25761  brsset  25765  brbigcup  25774  dffix2  25781  elfuns  25791  brimageg  25803  brdomaing  25811  brrangeg  25812  brimg  25813  brapply  25814  brsuccf  25817  funpartlem  25818  brrestrict  25825  dfrdg4  25826  axlowdim2  25930  axlowdim  25931  axcontlem2  25935  axcontlem3  25936  axcontlem4  25937  axcontlem7  25940  axcontlem9  25942  axcontlem10  25943  axcontlem11  25944  axcontlem12  25945  brofs  25970  btwncomim  25978  btwnintr  25984  btwnexch3  25985  btwnexch2  25988  brifs  26008  brcolinear2  26023  colineardim1  26026  brfs  26044  btwnconn1  26066  segcon2  26070  seglerflx  26077  seglemin  26078  btwnsegle  26082  colinbtwnle  26083  broutsideof2  26087  fvray  26106  lineunray  26112  lineelsb2  26113  linerflx1  26114  supaddc  26269  supadd  26270  ltflcei  26271  lxflflp1  26273  heicant  26277  mblfinlem1  26279  mblfinlem2  26280  itg2addnclem  26294  itg2addnclem3  26296  itg2addnc  26297  itg2gt0cn  26298  ibladdnclem  26299  iblmulc2nc  26308  itgabsnc  26312  bddiblnc  26313  ftc1anclem5  26322  ftc1anclem7  26324  ftc1anclem8  26325  ftc1anc  26326  trer  26357  elicc3  26358  finminlem  26359  nn0prpwlem  26363  nn0prpw  26364  indexdom  26474  filbcmb  26480  fdc  26487  prdsbnd  26540  heiborlem3  26560  rrnequiv  26582  prtlem10  26752  lzenom  26866  fphpdo  26916  irrapxlem4  26926  pellexlem6  26935  infmrgelbi  26979  pellfundre  26982  pellfundlb  26985  monotoddzz  27044  zindbi  27047  divalgmodcl  27096  jm2.27  27117  rmydioph  27123  rpnnen3lem  27140  fnwe2lem2  27164  aomclem8  27174  hbtlem5  27347  hbt  27349  pmtrval  27409  pmtrrn  27414  pmtrfrn  27415  phisum  27533  stoweidlem5  27768  stoweidlem20  27783  stoweidlem26  27789  stoweidlem28  27791  stoweidlem29  27792  stoweidlem34  27797  wallispilem3  27830  stirlinglem13  27849  funressnfv  28006  dfdfat2  28009  tz6.12-afv  28051  isfrgra  28478  3vfriswmgra  28493  1to2vfriswmgra  28494  vdfrgra0  28510  vdgfrgra0  28511  sgnval  28616  bnj23  29181  bnj1185  29263  bnj1152  29465  bnj1418  29507  lubunNEW  29869  lsatcveq0  29928  lsatcv1  29944  oposlem  30079  opnlen0  30084  lub0N  30085  glb0N  30089  omllaw  30139  cmtbr4N  30151  cvrval  30165  cvrnbtwn  30167  cvrnbtwn2  30171  cvrnbtwn3  30172  cvrcon3b  30173  cvrnbtwn4  30175  atcvreq0  30210  atnle  30213  atlatmstc  30215  cvlexch1  30224  glbconN  30272  hlsuprexch  30276  exatleN  30299  cvratlem  30316  atcvrj0  30323  atcvrj2b  30327  atlelt  30333  cvrat4  30338  3dim1lem5  30361  3dim2  30363  3dim3  30364  ps-2  30373  llni  30403  llnn0  30411  llnle  30413  lplni  30427  lplni2  30432  lplnle  30435  lplnn0N  30442  llncvrlpln  30453  2llnjN  30462  lvoli  30470  lvoli3  30472  lvoli2  30476  lvoln0N  30486  4at  30508  lplncvrlvol  30511  2lplnj  30515  dalemcea  30555  dalem3  30559  psubspi  30642  linepsubN  30647  elpmap  30653  pmapsub  30663  lnatexN  30674  cdlema1N  30686  cdlemb  30689  elpadd  30694  paddvaln0N  30696  paddasslem5  30719  llnexchb2lem  30763  llnexch2N  30765  islhp  30891  lhpat3  30941  4atexlemex2  30966  4atex  30971  4atex2-0aOLDN  30973  4atex2-0cOLDN  30975  lautle  30979  lautcvr  30987  lauteq  30990  ldilval  31008  ltrnu  31016  trlval2  31058  trlne  31080  cdleme0ex1N  31118  cdleme0nex  31185  cdleme18d  31190  cdlemednuN  31195  cdleme25b  31249  cdleme25cv  31253  cdleme27b  31263  cdleme29b  31270  cdleme31sn  31275  cdleme31fv  31285  cdleme31fv2  31288  cdlemefrs29bpre0  31291  cdlemefr29bpre0N  31301  cdlemefr29clN  31302  cdlemefr32fvaN  31304  cdlemefr32fva1  31305  cdlemefs29pre00N  31307  cdlemefs32sn1aw  31309  cdlemefs29bpre0N  31311  cdlemefs29bpre1N  31312  cdlemefs29cpre1N  31313  cdlemefs29clN  31314  cdlemefs32fvaN  31317  cdlemefs32fva1  31318  cdleme41sn3a  31328  cdleme32fva  31332  cdleme32e  31340  cdleme35f  31349  cdleme40v  31364  cdleme42b  31373  trlord  31464  cdlemg1cex  31483  diaval  31928  diaeldm  31932  diaelrnN  31941  cdlemm10N  32014  dibglbN  32062  dicval  32072  dicfnN  32079  dicvalrelN  32081  dihval  32128  dihlsscpre  32130  dihglblem3N  32191  dihmeetlem2N  32195  djhcvat42  32311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-br 4238
  Copyright terms: Public domain W3C validator