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

Theorem breq1 4207
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 3976 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2501 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 4205 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 4205 . 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 1652    e. wcel 1725   <.cop 3809   class class class wbr 4204
This theorem is referenced by:  breq12  4209  breq1i  4211  breq1d  4214  nbrne2  4222  brab1  4249  pocl  4502  swopolem  4504  swopo  4505  solin  4518  sotrieq  4522  sotr2  4524  isso2i  4527  somo  4529  frirr  4551  fr2nr  4552  wereu2  4571  fr3nr  4751  dfwe2  4753  vtoclr  4913  frsn  4939  brcog  5030  brcogw  5032  opelcnvg  5043  dfdmf  5055  eldmg  5056  dfrnf  5099  dfres2  5184  imasng  5217  asymref2  5242  sotri2  5254  somin1  5261  coi1  5376  dffun6f  5459  funmo  5461  fun11  5507  fveq2  5719  nfunsn  5752  dffv2  5787  dff3  5873  f1ompt  5882  fmptco  5892  dff13  5995  foeqcnvco  6018  isorel  6037  soisores  6038  soisoi  6039  isocnv  6041  isotr  6047  isomin  6048  isoini  6049  isopolem  6056  isosolem  6058  f1oiso  6062  f1oiso2  6063  f1oweALT  6065  weniso  6066  caovordig  6243  caovordg  6245  caovord3d  6248  caovord  6249  caovord3  6251  caofrss  6328  caoftrn  6330  frxp  6447  poxp  6449  fnse  6454  brtpos2  6476  rntpos  6483  tpostpos  6490  fvopab5  6525  ertr  6911  ecopovsym  6997  ecopovtrn  6998  th3qlem2  7002  isfi  7122  en0  7161  en1  7165  endisj  7186  xpcomco  7189  sbth  7218  2pwne  7254  disjenex  7256  ssenen  7272  nneneq  7281  php  7282  sdom1  7299  isinf  7313  fineqvlem  7314  pssnn  7318  enp1i  7334  findcard  7338  findcard2  7339  findcard3  7341  frfi  7343  fiint  7374  marypha1lem  7429  supmo  7446  eqsup  7450  supub  7453  suplub  7454  supmaxlem  7458  suppr  7462  supisolem  7464  supisoex  7465  ordtypecbv  7475  ordtypelem3  7478  ordtypelem6  7481  ordtypelem7  7482  ordtypelem9  7484  ordtypelem10  7485  hartogslem1  7500  hartogs  7502  wemaplem1  7504  wemaplem2  7505  card2on  7511  card2inf  7512  elharval  7520  brwdom2  7530  wdomtr  7532  cantnfp1lem2  7624  cantnflem1  7634  wemapwe  7643  r111  7690  kardex  7807  karden  7808  isnumi  7822  tskwe  7826  cardid2  7829  cardonle  7833  cardne  7841  iscard2  7852  infxpenlem  7884  fodomfi2  7930  wdomfil  7931  wdomnumr  7934  alephsuc2  7950  infenaleph  7961  iunfictbso  7984  infpss  8086  cff1  8127  cfslb2n  8137  sornom  8146  fin4i  8167  isfin6  8169  isfin7  8170  isfin1-3  8255  fin1a2lem9  8277  fin1a2lem11  8279  hsmexlem4  8298  axcc2lem  8305  axcc4dom  8310  domtriomlem  8311  numthcor  8363  zorn2lem2  8366  zorn2lem3  8367  zorn2lem7  8371  zorn2g  8372  axdclem  8388  axdc  8390  brdom7disj  8398  brdom6disj  8399  uniimadom  8408  ondomon  8427  alephval2  8436  alephreg  8446  pwcfsdom  8447  elgch  8486  gchi  8488  fpwwe2lem12  8505  fpwwe2lem13  8506  pwfseqlem4  8526  winainflem  8557  winalim2  8560  tsken  8618  0tsk  8619  inar1  8639  tskord  8644  tskuni  8647  grudomon  8681  pinq  8793  nqereu  8795  enqeq  8800  ltbtwnnq  8844  ltrnq  8845  prcdnq  8859  prnmax  8861  genpnmax  8873  nqpr  8880  1idpr  8895  reclem2pr  8914  reclem3pr  8915  reclem4pr  8916  recexpr  8917  supexpr  8920  ltsosr  8958  1ne0sr  8960  ltasr  8964  supsrlem  8975  axpre-lttri  9029  axpre-lttrn  9030  axpre-ltadd  9031  axpre-sup  9033  lelttr  9154  ltordlem  9541  lt0ne0d  9581  fimaxre3  9946  lbreu  9947  lble  9949  sup2  9953  infm3  9956  suprleub  9961  supmul1  9962  supmullem1  9963  supmul  9965  nnsub  10027  nominpos  10193  nnunb  10206  arch  10207  nn0sub  10259  nn0n0n1ge2b  10270  zextle  10332  peano5uzti  10348  fzind  10357  btwnz  10361  uzval  10479  uzwo  10528  uzwoOLD  10529  nnwof  10532  uzinfmi  10544  ublbneg  10549  lbzbi  10553  zsupss  10554  uzsupss  10557  uzwo3  10558  zmax  10560  rebtwnz  10562  rpnnen1lem3  10591  xrltnsym  10719  xrlttri  10721  xrlttr  10722  xrlelttr  10735  nltpnft  10743  xrmaxlt  10758  xrmaxle  10760  qbtwnre  10774  qbtwnxr  10775  xltnegi  10791  xsubge0  10829  xlesubadd  10831  xmullem2  10833  xlemul1a  10856  xrinfmexpnf  10873  xrsupsslem  10874  xrinfmsslem  10875  xrub  10879  supxrunb1  10887  supxrunb2  10888  ixxval  10913  elixx1  10914  elioo2  10946  iccid  10950  icc0  10953  fzval  11034  elfz1  11037  elfznelfzo  11180  elfznelfzob  11181  flval  11191  fllelt  11194  flval2  11209  flval3  11210  flbi  11211  modid2  11259  fsequb2  11303  seqf1olem2  11351  sqlecan  11475  faclbnd4lem1  11572  sqrlem6  12041  01sqrex  12043  abslt  12106  absle  12107  rexanre  12138  rexico  12145  limsupgle  12259  limsupgre  12263  limsupbnd2  12265  rlim2lt  12279  rlim3  12280  ello12r  12299  ello1d  12305  elo12r  12310  rlimconst  12326  climshft  12358  rlimcn2  12372  o1rlimmul  12400  lo1le  12433  climsup  12451  caucvgrlem  12454  isumless  12613  divrcnv  12620  cvgrat  12648  rpnnen2lem10  12811  ruclem1  12818  ruclem2  12819  ruclem11  12827  ruclem12  12828  sqr2irr  12836  absdvdsb  12856  dvdsle  12883  dvdseq  12885  dvdsext  12888  divalglem8  12908  divalglem9  12909  divalglem10  12910  divalgmod  12914  ndvdssub  12915  sadcaddlem  12957  gcdcllem1  12999  gcdcllem2  13000  gcdcllem3  13001  gcdeq  13040  dvdssq  13048  nn0seqcvgd  13049  algcvgblem  13056  1nprm  13072  1idssfct  13073  isprm2lem  13074  isprm2  13075  dvdsprime  13080  nprm  13081  3prm  13084  dvdsprm  13087  coprm  13088  exprmfct  13098  isprm5  13100  maxprmfct  13101  eulerthlem2  13159  odzval  13165  pythagtriplem4  13181  pc2dvds  13240  pcprmpw2  13243  pcprmpw  13244  prmpwdvds  13260  pockthg  13262  unbenlem  13264  prmreclem4  13275  prmreclem5  13276  prmreclem6  13277  1arith  13283  vdwlem6  13342  vdwlem11  13347  vdwlem13  13349  ramtlecl  13356  ramub  13369  rami  13371  ramubcl  13374  0ram  13376  ram0  13378  prmlem0  13416  prmlem1a  13417  imasaddfnlem  13741  imasvscafn  13750  imasleval  13754  prslem  14376  drsdir  14380  drsdirfi  14383  isdrs2  14384  posi  14395  posasymb  14397  pltval3  14412  plelttr  14417  pospo  14418  lubprop  14425  luble  14426  lubid  14427  glbprop  14430  joinval2  14434  joinlem  14435  meetlem  14442  meetle  14445  latnlej  14485  isglbd  14532  lubub  14534  lubun  14538  clatleglb  14541  pospropd  14549  poslubmo  14561  poslubd  14562  tsrlin  14639  spwmo  14646  spwpr2  14648  spwpr4  14651  letsr  14660  dirge  14670  mndodcongi  15169  odeq  15176  odmulgeq  15181  gexnnod  15210  sylow1lem1  15220  pgpssslw  15236  sylow2a  15241  efgredeu  15372  efgred2  15373  gexex  15456  frgpnabllem2  15473  cyggenod  15482  dprdval  15549  ablfacrplem  15611  ablfac1c  15617  ablfac1eu  15619  ablfaclem3  15633  abvtrivd  15916  psrbagconcl  16426  psrbagconf1o  16427  gsumbagdiaglem  16428  psrmulcllem  16439  psrlidm  16455  psrridm  16456  psrass1  16457  psrcom  16460  mplmonmul  16515  coe1mul2  16650  coe1tmmul  16657  zlpir  16759  prmirredlem  16761  znleval  16823  ordtbas2  17243  ordtopn2  17247  ordtrest2lem  17255  pnfnei  17272  ordtt1  17431  ordthauslem  17435  2ndci  17499  2ndcsb  17500  2ndcredom  17501  2ndc1stc  17502  1stcrest  17504  2ndcctbss  17506  2ndcdisj  17507  2ndcsep  17510  lly1stc  17547  tx1stc  17670  ordthmeolem  17821  ufildom1  17946  xmetrtri2  18374  prdsxmetlem  18386  ssblex  18446  prdsbl  18509  comet  18531  stdbdxmet  18533  stdbdmopn  18536  met1stc  18539  dscmet  18608  metdstri  18869  metdscn  18874  xrhmeo  18959  bndth  18971  evth  18972  lebnumlem3  18976  pcovalg  19025  pco1  19028  pcocn  19030  pcopt  19035  pcopt2  19036  pcoass  19037  nmoleub3  19115  bcthlem5  19269  minveclem4c  19314  minveclem2  19315  minveclem3b  19317  minveclem4  19321  minveclem6  19323  pmltpclem1  19333  pmltpc  19335  ovollb2lem  19372  ovolctb  19374  ovolunlem1  19381  ovoliunlem1  19386  ovoliunlem2  19387  ovoliun2  19390  ovolshftlem1  19393  ovolscalem1  19397  ovolicc1  19400  ovolicc2lem3  19403  voliunlem2  19433  voliunlem3  19434  ioombl1lem4  19443  uniioovol  19459  uniioombllem2  19463  uniioombllem3  19465  uniioombllem6  19468  volsup2  19485  ismbfd  19520  mbfsup  19544  mbflimsup  19546  itg1climres  19594  mbfi1fseqlem4  19598  itg2lr  19610  itg2leub  19614  itg2seq  19622  itg2monolem1  19630  itg2monolem3  19632  itg2mono  19633  itg2i1fseq2  19636  itg2gt0  19640  itg2cnlem1  19641  itg2cnlem2  19642  itg2cn  19643  iblss  19684  itgless  19696  ibladdlem  19699  iblabsr  19709  iblmulc2  19710  itgabs  19714  ditgeq1  19723  dvferm2lem  19858  rolle  19862  dvlip2  19867  c1liplem1  19868  c1lip1  19869  dvfsumlem2  19899  dvfsumlem4  19901  mdegleb  19975  degltlem1  19983  plyco0  20099  plyeq0lem  20117  coeeq2  20149  dgrle  20150  dgradd2  20174  plydiveu  20203  aareccl  20231  aalioulem2  20238  aaliou3lem7  20254  psercnlem1  20329  pilem2  20356  pilem3  20357  logltb  20482  divlogrlim  20514  logcnlem3  20523  cxpaddlelem  20623  rlimcnp  20792  cxplim  20798  cxploglim  20804  scvxcvx  20812  ftalem1  20843  ftalem2  20844  isppw2  20886  vmappw  20887  sgmnncl  20918  sqff1o  20953  dvdsdivcl  20954  fsumdvdsdiaglem  20956  dvdsppwf1o  20959  dvdsflsumcom  20961  musum  20964  muinv  20966  dvdsmulf1o  20967  vmalelog  20977  vmasum  20988  logfac2  20989  perfectlem2  21002  bcmono  21049  bpos1lem  21054  bposlem9  21064  lgsmod  21093  lgsne0  21105  2sqlem6  21141  2sqlem8  21144  2sqlem10  21146  chtppilim  21157  rpvmasumlem  21169  dchrisumlema  21170  dchrisumlem2  21172  dchrvmasumlem1  21177  dchrvmasumiflem1  21183  dchrisum0flblem1  21190  dchrisum0flblem2  21191  dchrisum0  21202  rplogsum  21209  logsqvma  21224  pntpbnd1  21268  pntpbnd2  21269  pntibndlem3  21274  pntlemj  21285  pntlemi  21286  pntlem3  21291  pnt3  21294  ostth3  21320  usgra1v  21397  usgrafisindb0  21410  usgrafisindb1  21411  cusgra1v  21458  1conngra  21650  eupath2  21690  gxnval  21836  rngosn4  22003  rngoueqz  22006  nmoubi  22261  minvecolem2  22365  minvecolem3  22366  minvecolem4c  22369  minvecolem4  22370  minvecolem5  22371  minvecolem6  22372  htthlem  22408  chlimi  22725  chcompl  22733  hsn0elch  22738  cmbr3  23098  cmcm  23104  cmcm3  23105  lecm  23107  nmopub  23399  nmfnleub  23416  nmopun  23505  nmcexi  23517  cnlnadjlem7  23564  pjnmopi  23639  stle0i  23730  stlesi  23732  stm1i  23734  csmdsymi  23825  cvmd  23827  atcveq0  23839  atcv1  23871  atord  23879  atcvat2  23880  chirred  23886  mdsym  23903  mddmdin0i  23922  cdj1i  23924  fmptcof2  24064  isoun  24077  lt2addrd  24103  xlt2addrd  24112  xrofsup  24114  tleile  24177  toslub  24179  tosglb  24180  ofldadd  24226  ofldmul  24227  xrnarchi  24242  xrge0iifiso  24309  rge0scvg  24323  gsumesum  24439  esumfsup  24448  esumpinfval  24451  esumpcvgval  24456  esumcvg  24464  sigaclcu  24488  sigaclci  24503  unelsiga  24505  measvun  24551  voliune  24573  volfiniune  24574  orvcval2  24704  dstfrvel  24719  ballotlemfc0  24738  ballotlemfcc  24739  ballotlemsv  24755  ballotlemsf1o  24759  relexpindlem  25127  rtrclreclem.trans  25134  dedekind  25175  dedekindle  25176  dfdm5  25387  dfrn5  25388  trpredpred  25486  poseq  25508  nodense  25598  nocvxminlem  25599  nobnddown  25610  nofulllem4  25614  nofulllem5  25615  brpprod  25680  brsset  25684  brbigcup  25693  dffix2  25700  elfuns  25710  brimageg  25722  brdomaing  25730  brrangeg  25731  brimg  25732  brapply  25733  brsuccf  25736  funpartlem  25737  brrestrict  25744  dfrdg4  25745  axlowdim2  25847  axlowdim  25848  axcontlem2  25852  axcontlem3  25853  axcontlem4  25854  axcontlem7  25857  axcontlem9  25859  axcontlem10  25860  axcontlem11  25861  axcontlem12  25862  brofs  25887  btwncomim  25895  btwnintr  25901  btwnexch3  25902  btwnexch2  25905  brifs  25925  brcolinear2  25940  colineardim1  25943  brfs  25961  btwnconn1  25983  segcon2  25987  seglerflx  25994  seglemin  25995  btwnsegle  25999  colinbtwnle  26000  broutsideof2  26004  fvray  26023  lineunray  26029  lineelsb2  26030  linerflx1  26031  supaddc  26184  supadd  26185  ltflcei  26187  lxflflp1  26189  mblfinlem  26190  itg2addnclem  26202  itg2addnclem3  26204  itg2addnc  26205  itg2gt0cn  26206  ibladdnclem  26207  iblmulc2nc  26216  itgabsnc  26220  bddiblnc  26221  trer  26256  elicc3  26257  finminlem  26258  nn0prpwlem  26262  nn0prpw  26263  indexdom  26373  filbcmb  26379  fdc  26386  prdsbnd  26439  heiborlem3  26459  rrnequiv  26481  prtlem10  26651  lzenom  26765  fphpdo  26815  irrapxlem4  26825  pellexlem6  26834  infmrgelbi  26878  pellfundre  26881  pellfundlb  26884  monotoddzz  26943  zindbi  26946  divalgmodcl  26995  jm2.27  27016  rmydioph  27022  rpnnen3lem  27039  fnwe2lem2  27063  aomclem8  27074  hbtlem5  27247  hbt  27249  pmtrval  27309  pmtrrn  27314  pmtrfrn  27315  phisum  27433  stoweidlem5  27668  stoweidlem20  27683  stoweidlem26  27689  stoweidlem28  27691  stoweidlem29  27692  stoweidlem34  27697  wallispilem3  27730  stirlinglem13  27749  funressnfv  27906  dfdfat2  27909  tz6.12-afv  27951  swrdccat3  28104  swrdccat3b  28106  isfrgra  28238  3vfriswmgra  28253  1to2vfriswmgra  28254  vdfrgra0  28270  vdgfrgra0  28271  sgnval  28376  bnj23  28937  bnj1185  29019  bnj1152  29221  bnj1418  29263  lubunNEW  29610  lsatcveq0  29669  lsatcv1  29685  oposlem  29820  opnlen0  29825  lub0N  29826  glb0N  29830  omllaw  29880  cmtbr4N  29892  cvrval  29906  cvrnbtwn  29908  cvrnbtwn2  29912  cvrnbtwn3  29913  cvrcon3b  29914  cvrnbtwn4  29916  atcvreq0  29951  atnle  29954  atlatmstc  29956  cvlexch1  29965  glbconN  30013  hlsuprexch  30017  exatleN  30040  cvratlem  30057  atcvrj0  30064  atcvrj2b  30068  atlelt  30074  cvrat4  30079  3dim1lem5  30102  3dim2  30104  3dim3  30105  ps-2  30114  llni  30144  llnn0  30152  llnle  30154  lplni  30168  lplni2  30173  lplnle  30176  lplnn0N  30183  llncvrlpln  30194  2llnjN  30203  lvoli  30211  lvoli3  30213  lvoli2  30217  lvoln0N  30227  4at  30249  lplncvrlvol  30252  2lplnj  30256  dalemcea  30296  dalem3  30300  psubspi  30383  linepsubN  30388  elpmap  30394  pmapsub  30404  lnatexN  30415  cdlema1N  30427  cdlemb  30430  elpadd  30435  paddvaln0N  30437  paddasslem5  30460  llnexchb2lem  30504  llnexch2N  30506  islhp  30632  lhpat3  30682  4atexlemex2  30707  4atex  30712  4atex2-0aOLDN  30714  4atex2-0cOLDN  30716  lautle  30720  lautcvr  30728  lauteq  30731  ldilval  30749  ltrnu  30757  trlval2  30799  trlne  30821  cdleme0ex1N  30859  cdleme0nex  30926  cdleme18d  30931  cdlemednuN  30936  cdleme25b  30990  cdleme25cv  30994  cdleme27b  31004  cdleme29b  31011  cdleme31sn  31016  cdleme31fv  31026  cdleme31fv2  31029  cdlemefrs29bpre0  31032  cdlemefr29bpre0N  31042  cdlemefr29clN  31043  cdlemefr32fvaN  31045  cdlemefr32fva1  31046  cdlemefs29pre00N  31048  cdlemefs32sn1aw  31050  cdlemefs29bpre0N  31052  cdlemefs29bpre1N  31053  cdlemefs29cpre1N  31054  cdlemefs29clN  31055  cdlemefs32fvaN  31058  cdlemefs32fva1  31059  cdleme41sn3a  31069  cdleme32fva  31073  cdleme32e  31081  cdleme35f  31090  cdleme40v  31105  cdleme42b  31114  trlord  31205  cdlemg1cex  31224  diaval  31669  diaeldm  31673  diaelrnN  31682  cdlemm10N  31755  dibglbN  31803  dicval  31813  dicfnN  31820  dicvalrelN  31822  dihval  31869  dihlsscpre  31871  dihglblem3N  31932  dihmeetlem2N  31936  djhcvat42  32052
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205
  Copyright terms: Public domain W3C validator