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

Theorem breq1 4215
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 3984 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2502 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 4213 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 4213 . 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 3817   class class class wbr 4212
This theorem is referenced by:  breq12  4217  breq1i  4219  breq1d  4222  nbrne2  4230  brab1  4257  pocl  4510  swopolem  4512  swopo  4513  solin  4526  sotrieq  4530  sotr2  4532  isso2i  4535  somo  4537  frirr  4559  fr2nr  4560  wereu2  4579  fr3nr  4760  dfwe2  4762  vtoclr  4922  frsn  4948  brcog  5039  brcogw  5041  opelcnvg  5052  dfdmf  5064  eldmg  5065  dfrnf  5108  dfres2  5193  imasng  5226  asymref2  5251  sotri2  5263  somin1  5270  coi1  5385  dffun6f  5468  funmo  5470  fun11  5516  fveq2  5728  nfunsn  5761  dffv2  5796  dff3  5882  f1ompt  5891  fmptco  5901  dff13  6004  foeqcnvco  6027  isorel  6046  soisores  6047  soisoi  6048  isocnv  6050  isotr  6056  isomin  6057  isoini  6058  isopolem  6065  isosolem  6067  f1oiso  6071  f1oiso2  6072  f1oweALT  6074  weniso  6075  caovordig  6252  caovordg  6254  caovord3d  6257  caovord  6258  caovord3  6260  caofrss  6337  caoftrn  6339  frxp  6456  poxp  6458  fnse  6463  brtpos2  6485  rntpos  6492  tpostpos  6499  fvopab5  6534  ertr  6920  ecopovsym  7006  ecopovtrn  7007  th3qlem2  7011  isfi  7131  en0  7170  en1  7174  endisj  7195  xpcomco  7198  sbth  7227  2pwne  7263  disjenex  7265  ssenen  7281  nneneq  7290  php  7291  sdom1  7308  isinf  7322  fineqvlem  7323  pssnn  7327  enp1i  7343  findcard  7347  findcard2  7348  findcard3  7350  frfi  7352  fiint  7383  marypha1lem  7438  supmo  7457  eqsup  7461  supub  7464  suplub  7465  supmaxlem  7469  suppr  7473  supisolem  7475  supisoex  7476  ordtypecbv  7486  ordtypelem3  7489  ordtypelem6  7492  ordtypelem7  7493  ordtypelem9  7495  ordtypelem10  7496  hartogslem1  7511  hartogs  7513  wemaplem1  7515  wemaplem2  7516  card2on  7522  card2inf  7523  elharval  7531  brwdom2  7541  wdomtr  7543  cantnfp1lem2  7635  cantnflem1  7645  wemapwe  7654  r111  7701  kardex  7818  karden  7819  isnumi  7833  tskwe  7837  cardid2  7840  cardonle  7844  cardne  7852  iscard2  7863  infxpenlem  7895  fodomfi2  7941  wdomfil  7942  wdomnumr  7945  alephsuc2  7961  infenaleph  7972  iunfictbso  7995  infpss  8097  cff1  8138  cfslb2n  8148  sornom  8157  fin4i  8178  isfin6  8180  isfin7  8181  isfin1-3  8266  fin1a2lem9  8288  fin1a2lem11  8290  hsmexlem4  8309  axcc2lem  8316  axcc4dom  8321  domtriomlem  8322  numthcor  8374  zorn2lem2  8377  zorn2lem3  8378  zorn2lem7  8382  zorn2g  8383  axdclem  8399  axdc  8401  brdom7disj  8409  brdom6disj  8410  uniimadom  8419  ondomon  8438  alephval2  8447  alephreg  8457  pwcfsdom  8458  elgch  8497  gchi  8499  fpwwe2lem12  8516  fpwwe2lem13  8517  pwfseqlem4  8537  winainflem  8568  winalim2  8571  tsken  8629  0tsk  8630  inar1  8650  tskord  8655  tskuni  8658  grudomon  8692  pinq  8804  nqereu  8806  enqeq  8811  ltbtwnnq  8855  ltrnq  8856  prcdnq  8870  prnmax  8872  genpnmax  8884  nqpr  8891  1idpr  8906  reclem2pr  8925  reclem3pr  8926  reclem4pr  8927  recexpr  8928  supexpr  8931  ltsosr  8969  1ne0sr  8971  ltasr  8975  supsrlem  8986  axpre-lttri  9040  axpre-lttrn  9041  axpre-ltadd  9042  axpre-sup  9044  lelttr  9165  ltordlem  9552  lt0ne0d  9592  fimaxre3  9957  lbreu  9958  lble  9960  sup2  9964  infm3  9967  suprleub  9972  supmul1  9973  supmullem1  9974  supmul  9976  nnsub  10038  nominpos  10204  nnunb  10217  arch  10218  nn0sub  10270  nn0n0n1ge2b  10281  zextle  10343  peano5uzti  10359  fzind  10368  btwnz  10372  uzval  10490  uzwo  10539  uzwoOLD  10540  nnwof  10543  uzinfmi  10555  ublbneg  10560  lbzbi  10564  zsupss  10565  uzsupss  10568  uzwo3  10569  zmax  10571  rebtwnz  10573  rpnnen1lem3  10602  xrltnsym  10730  xrlttri  10732  xrlttr  10733  xrlelttr  10746  nltpnft  10754  xrmaxlt  10769  xrmaxle  10771  qbtwnre  10785  qbtwnxr  10786  xltnegi  10802  xsubge0  10840  xlesubadd  10842  xmullem2  10844  xlemul1a  10867  xrinfmexpnf  10884  xrsupsslem  10885  xrinfmsslem  10886  xrub  10890  supxrunb1  10898  supxrunb2  10899  ixxval  10924  elixx1  10925  elioo2  10957  iccid  10961  icc0  10964  fzval  11045  elfz1  11048  elfznelfzo  11192  elfznelfzob  11193  flval  11203  fllelt  11206  flval2  11221  flval3  11222  flbi  11223  modid2  11271  fsequb2  11315  seqf1olem2  11363  sqlecan  11487  faclbnd4lem1  11584  sqrlem6  12053  01sqrex  12055  abslt  12118  absle  12119  rexanre  12150  rexico  12157  limsupgle  12271  limsupgre  12275  limsupbnd2  12277  rlim2lt  12291  rlim3  12292  ello12r  12311  ello1d  12317  elo12r  12322  rlimconst  12338  climshft  12370  rlimcn2  12384  o1rlimmul  12412  lo1le  12445  climsup  12463  caucvgrlem  12466  isumless  12625  divrcnv  12632  cvgrat  12660  rpnnen2lem10  12823  ruclem1  12830  ruclem2  12831  ruclem11  12839  ruclem12  12840  sqr2irr  12848  absdvdsb  12868  dvdsle  12895  dvdseq  12897  dvdsext  12900  divalglem8  12920  divalglem9  12921  divalglem10  12922  divalgmod  12926  ndvdssub  12927  sadcaddlem  12969  gcdcllem1  13011  gcdcllem2  13012  gcdcllem3  13013  gcdeq  13052  dvdssq  13060  nn0seqcvgd  13061  algcvgblem  13068  1nprm  13084  1idssfct  13085  isprm2lem  13086  isprm2  13087  dvdsprime  13092  nprm  13093  3prm  13096  dvdsprm  13099  coprm  13100  exprmfct  13110  isprm5  13112  maxprmfct  13113  eulerthlem2  13171  odzval  13177  pythagtriplem4  13193  pc2dvds  13252  pcprmpw2  13255  pcprmpw  13256  prmpwdvds  13272  pockthg  13274  unbenlem  13276  prmreclem4  13287  prmreclem5  13288  prmreclem6  13289  1arith  13295  vdwlem6  13354  vdwlem11  13359  vdwlem13  13361  ramtlecl  13368  ramub  13381  rami  13383  ramubcl  13386  0ram  13388  ram0  13390  prmlem0  13428  prmlem1a  13429  imasaddfnlem  13753  imasvscafn  13762  imasleval  13766  prslem  14388  drsdir  14392  drsdirfi  14395  isdrs2  14396  posi  14407  posasymb  14409  pltval3  14424  plelttr  14429  pospo  14430  lubprop  14437  luble  14438  lubid  14439  glbprop  14442  joinval2  14446  joinlem  14447  meetlem  14454  meetle  14457  latnlej  14497  isglbd  14544  lubub  14546  lubun  14550  clatleglb  14553  pospropd  14561  poslubmo  14573  poslubd  14574  tsrlin  14651  spwmo  14658  spwpr2  14660  spwpr4  14663  letsr  14672  dirge  14682  mndodcongi  15181  odeq  15188  odmulgeq  15193  gexnnod  15222  sylow1lem1  15232  pgpssslw  15248  sylow2a  15253  efgredeu  15384  efgred2  15385  gexex  15468  frgpnabllem2  15485  cyggenod  15494  dprdval  15561  ablfacrplem  15623  ablfac1c  15629  ablfac1eu  15631  ablfaclem3  15645  abvtrivd  15928  psrbagconcl  16438  psrbagconf1o  16439  gsumbagdiaglem  16440  psrmulcllem  16451  psrlidm  16467  psrridm  16468  psrass1  16469  psrcom  16472  mplmonmul  16527  coe1mul2  16662  coe1tmmul  16669  zlpir  16771  prmirredlem  16773  znleval  16835  ordtbas2  17255  ordtopn2  17259  ordtrest2lem  17267  pnfnei  17284  ordtt1  17443  ordthauslem  17447  2ndci  17511  2ndcsb  17512  2ndcredom  17513  2ndc1stc  17514  1stcrest  17516  2ndcctbss  17518  2ndcdisj  17519  2ndcsep  17522  lly1stc  17559  tx1stc  17682  ordthmeolem  17833  ufildom1  17958  xmetrtri2  18386  prdsxmetlem  18398  ssblex  18458  prdsbl  18521  comet  18543  stdbdxmet  18545  stdbdmopn  18548  met1stc  18551  dscmet  18620  metdstri  18881  metdscn  18886  xrhmeo  18971  bndth  18983  evth  18984  lebnumlem3  18988  pcovalg  19037  pco1  19040  pcocn  19042  pcopt  19047  pcopt2  19048  pcoass  19049  nmoleub3  19127  bcthlem5  19281  minveclem4c  19326  minveclem2  19327  minveclem3b  19329  minveclem4  19333  minveclem6  19335  pmltpclem1  19345  pmltpc  19347  ovollb2lem  19384  ovolctb  19386  ovolunlem1  19393  ovoliunlem1  19398  ovoliunlem2  19399  ovoliun2  19402  ovolshftlem1  19405  ovolscalem1  19409  ovolicc1  19412  ovolicc2lem3  19415  voliunlem2  19445  voliunlem3  19446  ioombl1lem4  19455  uniioovol  19471  uniioombllem2  19475  uniioombllem3  19477  uniioombllem6  19480  volsup2  19497  ismbfd  19532  mbfsup  19556  mbflimsup  19558  itg1climres  19606  mbfi1fseqlem4  19610  itg2lr  19622  itg2leub  19626  itg2seq  19634  itg2monolem1  19642  itg2monolem3  19644  itg2mono  19645  itg2i1fseq2  19648  itg2gt0  19652  itg2cnlem1  19653  itg2cnlem2  19654  itg2cn  19655  iblss  19696  itgless  19708  ibladdlem  19711  iblabsr  19721  iblmulc2  19722  itgabs  19726  ditgeq1  19735  dvferm2lem  19870  rolle  19874  dvlip2  19879  c1liplem1  19880  c1lip1  19881  dvfsumlem2  19911  dvfsumlem4  19913  mdegleb  19987  degltlem1  19995  plyco0  20111  plyeq0lem  20129  coeeq2  20161  dgrle  20162  dgradd2  20186  plydiveu  20215  aareccl  20243  aalioulem2  20250  aaliou3lem7  20266  psercnlem1  20341  pilem2  20368  pilem3  20369  logltb  20494  divlogrlim  20526  logcnlem3  20535  cxpaddlelem  20635  rlimcnp  20804  cxplim  20810  cxploglim  20816  scvxcvx  20824  ftalem1  20855  ftalem2  20856  isppw2  20898  vmappw  20899  sgmnncl  20930  sqff1o  20965  dvdsdivcl  20966  fsumdvdsdiaglem  20968  dvdsppwf1o  20971  dvdsflsumcom  20973  musum  20976  muinv  20978  dvdsmulf1o  20979  vmalelog  20989  vmasum  21000  logfac2  21001  perfectlem2  21014  bcmono  21061  bpos1lem  21066  bposlem9  21076  lgsmod  21105  lgsne0  21117  2sqlem6  21153  2sqlem8  21156  2sqlem10  21158  chtppilim  21169  rpvmasumlem  21181  dchrisumlema  21182  dchrisumlem2  21184  dchrvmasumlem1  21189  dchrvmasumiflem1  21195  dchrisum0flblem1  21202  dchrisum0flblem2  21203  dchrisum0  21214  rplogsum  21221  logsqvma  21236  pntpbnd1  21280  pntpbnd2  21281  pntibndlem3  21286  pntlemj  21297  pntlemi  21298  pntlem3  21303  pnt3  21306  ostth3  21332  usgra1v  21409  usgrafisindb0  21422  usgrafisindb1  21423  cusgra1v  21470  1conngra  21662  eupath2  21702  gxnval  21848  rngosn4  22015  rngoueqz  22018  nmoubi  22273  minvecolem2  22377  minvecolem3  22378  minvecolem4c  22381  minvecolem4  22382  minvecolem5  22383  minvecolem6  22384  htthlem  22420  chlimi  22737  chcompl  22745  hsn0elch  22750  cmbr3  23110  cmcm  23116  cmcm3  23117  lecm  23119  nmopub  23411  nmfnleub  23428  nmopun  23517  nmcexi  23529  cnlnadjlem7  23576  pjnmopi  23651  stle0i  23742  stlesi  23744  stm1i  23746  csmdsymi  23837  cvmd  23839  atcveq0  23851  atcv1  23883  atord  23891  atcvat2  23892  chirred  23898  mdsym  23915  mddmdin0i  23934  cdj1i  23936  fmptcof2  24076  isoun  24089  lt2addrd  24115  xlt2addrd  24124  xrofsup  24126  tleile  24189  toslub  24191  tosglb  24192  ofldadd  24238  ofldmul  24239  xrnarchi  24254  xrge0iifiso  24321  rge0scvg  24335  gsumesum  24451  esumfsup  24460  esumpinfval  24463  esumpcvgval  24468  esumcvg  24476  sigaclcu  24500  sigaclci  24515  unelsiga  24517  measvun  24563  voliune  24585  volfiniune  24586  orvcval2  24716  dstfrvel  24731  ballotlemfc0  24750  ballotlemfcc  24751  ballotlemsv  24767  ballotlemsf1o  24771  relexpindlem  25139  rtrclreclem.trans  25146  dedekind  25187  dedekindle  25188  dfdm5  25400  dfrn5  25401  trpredpred  25506  poseq  25528  wsuclem  25576  nodense  25644  nocvxminlem  25645  nobnddown  25656  nofulllem4  25660  nofulllem5  25661  brpprod  25730  brsset  25734  brbigcup  25743  dffix2  25750  elfuns  25760  brimageg  25772  brdomaing  25780  brrangeg  25781  brimg  25782  brapply  25783  brsuccf  25786  funpartlem  25787  brrestrict  25794  dfrdg4  25795  axlowdim2  25899  axlowdim  25900  axcontlem2  25904  axcontlem3  25905  axcontlem4  25906  axcontlem7  25909  axcontlem9  25911  axcontlem10  25912  axcontlem11  25913  axcontlem12  25914  brofs  25939  btwncomim  25947  btwnintr  25953  btwnexch3  25954  btwnexch2  25957  brifs  25977  brcolinear2  25992  colineardim1  25995  brfs  26013  btwnconn1  26035  segcon2  26039  seglerflx  26046  seglemin  26047  btwnsegle  26051  colinbtwnle  26052  broutsideof2  26056  fvray  26075  lineunray  26081  lineelsb2  26082  linerflx1  26083  supaddc  26237  supadd  26238  ltflcei  26239  lxflflp1  26241  mblfinlem1  26243  mblfinlem2  26244  itg2addnclem  26256  itg2addnclem3  26258  itg2addnc  26259  itg2gt0cn  26260  ibladdnclem  26261  iblmulc2nc  26270  itgabsnc  26274  bddiblnc  26275  ftc1anclem5  26284  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  trer  26319  elicc3  26320  finminlem  26321  nn0prpwlem  26325  nn0prpw  26326  indexdom  26436  filbcmb  26442  fdc  26449  prdsbnd  26502  heiborlem3  26522  rrnequiv  26544  prtlem10  26714  lzenom  26828  fphpdo  26878  irrapxlem4  26888  pellexlem6  26897  infmrgelbi  26941  pellfundre  26944  pellfundlb  26947  monotoddzz  27006  zindbi  27009  divalgmodcl  27058  jm2.27  27079  rmydioph  27085  rpnnen3lem  27102  fnwe2lem2  27126  aomclem8  27136  hbtlem5  27309  hbt  27311  pmtrval  27371  pmtrrn  27376  pmtrfrn  27377  phisum  27495  stoweidlem5  27730  stoweidlem20  27745  stoweidlem26  27751  stoweidlem28  27753  stoweidlem29  27754  stoweidlem34  27759  wallispilem3  27792  stirlinglem13  27811  funressnfv  27968  dfdfat2  27971  tz6.12-afv  28013  isfrgra  28380  3vfriswmgra  28395  1to2vfriswmgra  28396  vdfrgra0  28412  vdgfrgra0  28413  sgnval  28518  bnj23  29083  bnj1185  29165  bnj1152  29367  bnj1418  29409  lubunNEW  29771  lsatcveq0  29830  lsatcv1  29846  oposlem  29981  opnlen0  29986  lub0N  29987  glb0N  29991  omllaw  30041  cmtbr4N  30053  cvrval  30067  cvrnbtwn  30069  cvrnbtwn2  30073  cvrnbtwn3  30074  cvrcon3b  30075  cvrnbtwn4  30077  atcvreq0  30112  atnle  30115  atlatmstc  30117  cvlexch1  30126  glbconN  30174  hlsuprexch  30178  exatleN  30201  cvratlem  30218  atcvrj0  30225  atcvrj2b  30229  atlelt  30235  cvrat4  30240  3dim1lem5  30263  3dim2  30265  3dim3  30266  ps-2  30275  llni  30305  llnn0  30313  llnle  30315  lplni  30329  lplni2  30334  lplnle  30337  lplnn0N  30344  llncvrlpln  30355  2llnjN  30364  lvoli  30372  lvoli3  30374  lvoli2  30378  lvoln0N  30388  4at  30410  lplncvrlvol  30413  2lplnj  30417  dalemcea  30457  dalem3  30461  psubspi  30544  linepsubN  30549  elpmap  30555  pmapsub  30565  lnatexN  30576  cdlema1N  30588  cdlemb  30591  elpadd  30596  paddvaln0N  30598  paddasslem5  30621  llnexchb2lem  30665  llnexch2N  30667  islhp  30793  lhpat3  30843  4atexlemex2  30868  4atex  30873  4atex2-0aOLDN  30875  4atex2-0cOLDN  30877  lautle  30881  lautcvr  30889  lauteq  30892  ldilval  30910  ltrnu  30918  trlval2  30960  trlne  30982  cdleme0ex1N  31020  cdleme0nex  31087  cdleme18d  31092  cdlemednuN  31097  cdleme25b  31151  cdleme25cv  31155  cdleme27b  31165  cdleme29b  31172  cdleme31sn  31177  cdleme31fv  31187  cdleme31fv2  31190  cdlemefrs29bpre0  31193  cdlemefr29bpre0N  31203  cdlemefr29clN  31204  cdlemefr32fvaN  31206  cdlemefr32fva1  31207  cdlemefs29pre00N  31209  cdlemefs32sn1aw  31211  cdlemefs29bpre0N  31213  cdlemefs29bpre1N  31214  cdlemefs29cpre1N  31215  cdlemefs29clN  31216  cdlemefs32fvaN  31219  cdlemefs32fva1  31220  cdleme41sn3a  31230  cdleme32fva  31234  cdleme32e  31242  cdleme35f  31251  cdleme40v  31266  cdleme42b  31275  trlord  31366  cdlemg1cex  31385  diaval  31830  diaeldm  31834  diaelrnN  31843  cdlemm10N  31916  dibglbN  31964  dicval  31974  dicfnN  31981  dicvalrelN  31983  dihval  32030  dihlsscpre  32032  dihglblem3N  32093  dihmeetlem2N  32097  djhcvat42  32213
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator