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

Theorem breq1 4296
Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
breq1 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))

Proof of Theorem breq1
StepHypRef Expression
1 opeq1 4061 . . 3 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
21eleq1d 2545 . 2 (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3 df-br 4294 . 2 (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4 df-br 4294 . 2 (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
52, 3, 43bitr4g 281 1 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 178   = wceq 1662  wcel 1734  cop 3891   class class class wbr 4293
This theorem is referenced by:  breq12  4298  breq1i  4300  breq1d  4303  nbrne2  4311  brab1  4338  pocl  4602  swopolem  4604  swopo  4605  solin  4618  sotrieq  4622  sotr2  4624  isso2i  4627  somo  4629  frirr  4651  fr2nr  4652  wereu2  4671  fr3nr  4852  dfwe2  4854  vtoclr  5013  frsn  5039  brcog  5132  brcogw  5134  opelcnvg  5145  dfdmf  5159  eldmg  5160  dfrnf  5203  dfres2  5288  imasng  5321  asymref2  5346  sotri2  5358  somin1  5365  coi1  5483  dffun6f  5567  funmo  5569  fun11  5615  fveq2  5827  nfunsn  5856  dffv2  5896  dff3  5982  f1ompt  5991  fmptco  6001  dff13  6104  foeqcnvco  6127  isorel  6146  soisores  6147  soisoi  6148  isocnv  6150  isotr  6156  isomin  6157  isoini  6158  isopolem  6165  isosolem  6167  f1oiso  6171  f1oiso2  6172  f1oweALT  6174  weniso  6175  caovordig  6354  caovordg  6356  caovord3d  6359  caovord  6360  caovord3  6362  caofrss  6439  caoftrn  6441  frxp  6560  poxp  6562  fnse  6567  brtpos2  6589  rntpos  6596  tpostpos  6603  fvopab5  6638  ertr  7015  ecopovsym  7101  ecopovtrn  7102  th3qlem2  7106  isfi  7226  en0  7265  en1  7269  endisj  7290  xpcomco  7293  sbth  7322  2pwne  7358  disjenex  7360  ssenen  7376  nneneq  7385  php  7386  sdom1  7403  isinf  7417  fineqvlem  7418  pssnn  7422  enp1i  7438  findcard  7442  findcard2  7443  findcard3  7445  frfi  7447  fiint  7478  marypha1lem  7533  supmo  7552  eqsup  7556  supub  7559  suplub  7560  supmaxlem  7564  suppr  7568  supisolem  7570  supisoex  7571  ordtypecbv  7581  ordtypelem3  7584  ordtypelem6  7587  ordtypelem7  7588  ordtypelem9  7590  ordtypelem10  7591  hartogslem1  7606  hartogs  7608  wemaplem1  7610  wemaplem2  7611  card2on  7617  card2inf  7618  elharval  7626  brwdom2  7636  wdomtr  7638  cantnfp1lem2  7730  cantnflem1  7740  wemapwe  7749  r111  7796  kardex  7915  karden  7916  isnumi  7930  tskwe  7934  cardid2  7937  cardonle  7941  cardne  7949  iscard2  7960  infxpenlem  7992  fodomfi2  8038  wdomfil  8039  wdomnumr  8042  alephsuc2  8058  infenaleph  8069  iunfictbso  8092  infpss  8194  cff1  8235  cfslb2n  8245  sornom  8254  fin4i  8275  isfin6  8277  isfin7  8278  isfin1-3  8363  fin1a2lem9  8385  fin1a2lem11  8387  hsmexlem4  8406  axcc2lem  8413  axcc4dom  8418  domtriomlem  8419  numthcor  8471  zorn2lem2  8474  zorn2lem3  8475  zorn2lem7  8479  zorn2g  8480  axdclem  8496  axdc  8498  brdom7disj  8506  brdom6disj  8507  uniimadom  8516  ondomon  8535  alephval2  8544  alephreg  8554  pwcfsdom  8555  elgch  8594  gchi  8596  fpwwe2lem12  8613  fpwwe2lem13  8614  pwfseqlem4  8634  winainflem  8665  winalim2  8668  tsken  8726  0tsk  8727  inar1  8747  tskord  8752  tskuni  8755  grudomon  8789  pinq  8901  nqereu  8903  enqeq  8908  ltbtwnnq  8952  ltrnq  8953  prcdnq  8967  prnmax  8969  genpnmax  8981  nqpr  8988  1idpr  9003  reclem2pr  9022  reclem3pr  9023  reclem4pr  9024  recexpr  9025  supexpr  9028  ltsosr  9066  1ne0sr  9068  ltasr  9072  supsrlem  9083  axpre-lttri  9137  axpre-lttrn  9138  axpre-ltadd  9139  axpre-sup  9141  lelttr  9263  ltordlem  9650  lt0ne0d  9690  fimaxre3  10055  lbreu  10056  lble  10058  sup2  10062  infm3  10065  suprleub  10070  supmul1  10071  supmullem1  10072  supmul  10074  nnsub  10136  nominpos  10302  nnunb  10315  arch  10316  nn0sub  10368  nn0n0n1ge2b  10379  zextle  10441  peano5uzti  10457  fzind  10466  btwnz  10470  uzval  10588  uzwo  10638  uzwoOLD  10639  nnwof  10642  uzinfmi  10655  ublbneg  10660  lbzbi  10664  zsupss  10665  uzsupss  10668  uzwo3  10669  zmax  10671  rebtwnz  10673  rpnnen1lem3  10702  xrltnsym  10830  xrlttri  10832  xrlttr  10833  xrlelttr  10846  nltpnft  10854  xrmaxlt  10869  xrmaxle  10871  qbtwnre  10885  qbtwnxr  10886  xltnegi  10902  xsubge0  10940  xlesubadd  10942  xmullem2  10944  xlemul1a  10967  xrinfmexpnf  10984  xrsupsslem  10985  xrinfmsslem  10986  xrub  10990  supxrunb1  10998  supxrunb2  10999  ixxval  11024  elixx1  11025  elioo2  11057  iccid  11061  icc0  11064  fzval  11145  elfz1  11148  elfznelfzo  11294  elfznelfzob  11295  flval  11305  fllelt  11308  flval2  11323  flval3  11324  flbi  11325  modid2  11373  fsequb2  11419  seqf1olem2  11467  sqlecan  11591  faclbnd4lem1  11688  sgnval  12013  sqrlem6  12173  01sqrex  12175  abslt  12238  absle  12239  rexanre  12270  rexico  12277  limsupgle  12391  limsupgre  12395  limsupbnd2  12397  rlim2lt  12411  rlim3  12412  ello12r  12431  ello1d  12437  elo12r  12442  rlimconst  12458  climshft  12490  rlimcn2  12504  o1rlimmul  12532  lo1le  12565  climsup  12583  caucvgrlem  12586  isumless  12745  divrcnv  12752  cvgrat  12780  rpnnen2lem10  12943  ruclem1  12950  ruclem2  12951  ruclem11  12959  ruclem12  12960  sqr2irr  12968  absdvdsb  12988  dvdsle  13015  dvdseq  13017  dvdsext  13020  divalglem8  13040  divalglem9  13041  divalglem10  13042  divalgmod  13046  ndvdssub  13047  sadcaddlem  13089  gcdcllem1  13131  gcdcllem2  13132  gcdcllem3  13133  gcdeq  13172  dvdssq  13180  nn0seqcvgd  13181  algcvgblem  13188  1nprm  13204  1idssfct  13205  isprm2lem  13206  isprm2  13207  dvdsprime  13212  nprm  13213  3prm  13216  dvdsprm  13219  coprm  13220  exprmfct  13230  isprm5  13232  maxprmfct  13233  eulerthlem2  13291  odzval  13297  pythagtriplem4  13313  pc2dvds  13372  pcprmpw2  13375  pcprmpw  13376  prmpwdvds  13392  pockthg  13394  unbenlem  13396  prmreclem4  13407  prmreclem5  13408  prmreclem6  13409  1arith  13415  vdwlem6  13474  vdwlem11  13479  vdwlem13  13481  ramtlecl  13488  ramub  13501  rami  13503  ramubcl  13506  0ram  13508  ram0  13510  prmlem0  13548  prmlem1a  13549  imasaddfnlem  13873  imasvscafn  13882  imasleval  13886  prslem  14508  drsdir  14512  drsdirfi  14515  isdrs2  14516  posi  14527  posasymb  14529  pltval3  14544  plelttr  14549  pospo  14550  lubprop  14563  luble  14564  lublecllem  14565  glbprop  14576  joinval2lem  14585  joinlem  14588  meetlem  14602  meetle  14605  latnlej  14645  isglbd  14694  lubub  14696  lubun  14700  clatleglb  14703  pospropd  14711  poslubmo  14723  posglbmo  14724  poslubd  14725  tsrlin  14796  letsr  14804  dirge  14814  mndodcongi  15313  odeq  15320  odmulgeq  15325  gexnnod  15354  sylow1lem1  15364  pgpssslw  15380  sylow2a  15385  efgredeu  15516  efgred2  15517  gexex  15600  frgpnabllem2  15617  cyggenod  15626  dprdval  15693  ablfacrplem  15755  ablfac1c  15761  ablfac1eu  15763  ablfaclem3  15777  abvtrivd  16060  psrbagconcl  16570  psrbagconf1o  16571  gsumbagdiaglem  16572  psrmulcllem  16583  psrlidm  16599  psrridm  16600  psrass1  16601  psrcom  16604  mplmonmul  16659  coe1mul2  16794  coe1tmmul  16801  zlpir  16903  prmirredlem  16905  znleval  16967  ordtbas2  17387  ordtopn2  17391  ordtrest2lem  17399  pnfnei  17416  ordtt1  17575  ordthauslem  17579  2ndci  17643  2ndcsb  17644  2ndcredom  17645  2ndc1stc  17646  1stcrest  17648  2ndcctbss  17650  2ndcdisj  17651  2ndcsep  17654  lly1stc  17691  tx1stc  17814  ordthmeolem  17965  ufildom1  18090  xmetrtri2  18518  prdsxmetlem  18530  ssblex  18590  prdsbl  18653  comet  18675  stdbdxmet  18677  stdbdmopn  18680  met1stc  18683  dscmet  18752  metdstri  19013  metdscn  19018  xrhmeo  19103  bndth  19115  evth  19116  lebnumlem3  19120  pcovalg  19169  pco1  19172  pcocn  19174  pcopt  19179  pcopt2  19180  pcoass  19181  nmoleub3  19259  bcthlem5  19413  minveclem4c  19458  minveclem2  19459  minveclem3b  19461  minveclem4  19465  minveclem6  19467  pmltpclem1  19477  pmltpc  19479  ovollb2lem  19516  ovolctb  19518  ovolunlem1  19525  ovoliunlem1  19530  ovoliunlem2  19531  ovoliun2  19534  ovolshftlem1  19537  ovolscalem1  19541  ovolicc1  19544  ovolicc2lem3  19547  voliunlem2  19577  voliunlem3  19578  ioombl1lem4  19587  uniioovol  19603  uniioombllem2  19607  uniioombllem3  19609  uniioombllem6  19612  volsup2  19629  ismbfd  19662  mbfsup  19686  mbflimsup  19688  itg1climres  19736  mbfi1fseqlem4  19740  itg2lr  19752  itg2leub  19756  itg2seq  19764  itg2monolem1  19772  itg2monolem3  19774  itg2mono  19775  itg2i1fseq2  19778  itg2gt0  19782  itg2cnlem1  19783  itg2cnlem2  19784  itg2cn  19785  iblss  19826  itgless  19838  ibladdlem  19841  iblabsr  19851  iblmulc2  19852  itgabs  19856  ditgeq1  19867  dvferm2lem  20002  rolle  20006  dvlip2  20011  c1liplem1  20012  c1lip1  20013  dvfsumlem2  20043  dvfsumlem4  20045  mdegleb  20119  degltlem1  20127  plyco0  20243  plyeq0lem  20261  coeeq2  20293  dgrle  20294  dgradd2  20318  plydiveu  20347  aareccl  20375  aalioulem2  20382  aaliou3lem7  20398  psercnlem1  20473  pilem2  20500  pilem3  20501  logltb  20626  divlogrlim  20658  logcnlem3  20667  cxpaddlelem  20767  rlimcnp  20936  cxplim  20942  cxploglim  20948  scvxcvx  20956  ftalem1  20987  ftalem2  20988  isppw2  21030  vmappw  21031  sgmnncl  21062  sqff1o  21097  dvdsdivcl  21098  fsumdvdsdiaglem  21100  dvdsppwf1o  21103  dvdsflsumcom  21105  musum  21108  muinv  21110  dvdsmulf1o  21111  vmalelog  21121  vmasum  21132  logfac2  21133  perfectlem2  21146  bcmono  21193  bpos1lem  21198  bposlem9  21208  lgsmod  21237  lgsne0  21249  2sqlem6  21285  2sqlem8  21288  2sqlem10  21290  chtppilim  21301  rpvmasumlem  21313  dchrisumlema  21314  dchrisumlem2  21316  dchrvmasumlem1  21321  dchrvmasumiflem1  21327  dchrisum0flblem1  21334  dchrisum0flblem2  21335  dchrisum0  21346  rplogsum  21353  logsqvma  21368  pntpbnd1  21412  pntpbnd2  21413  pntibndlem3  21418  pntlemj  21429  pntlemi  21430  pntlem3  21435  pnt3  21438  ostth3  21464  usgra1v  21541  usgrafisindb0  21554  usgrafisindb1  21555  cusgra1v  21602  1conngra  21794  eupath2  21834  gxnval  21980  rngosn4  22147  rngoueqz  22150  nmoubi  22405  minvecolem2  22509  minvecolem3  22510  minvecolem4c  22513  minvecolem4  22514  minvecolem5  22515  minvecolem6  22516  htthlem  22552  chlimi  22869  chcompl  22877  hsn0elch  22882  cmbr3  23242  cmcm  23248  cmcm3  23249  lecm  23251  nmopub  23543  nmfnleub  23560  nmopun  23649  nmcexi  23661  cnlnadjlem7  23708  pjnmopi  23783  stle0i  23874  stlesi  23876  stm1i  23878  csmdsymi  23969  cvmd  23971  atcveq0  23983  atcv1  24015  atord  24023  atcvat2  24024  chirred  24030  mdsym  24047  mddmdin0i  24066  cdj1i  24068  fmptcof2  24224  isoun  24242  lt2addrd  24281  xlt2addrd  24296  xrofsup  24298  tleile  24371  toslublem  24377  tosglblem  24379  omndadd  24419  xrnarchi  24451  archirng  24455  archiexdiv  24457  archiabl  24465  isarchiofld  24564  ordtrest2NEWlem  24649  ordtconlem1  24651  xrge0iifiso  24662  rge0scvg  24676  gsumesum  24808  esumfsup  24817  esumpinfval  24820  esumpcvgval  24825  esumcvg  24833  sigaclcu  24858  sigaclci  24873  unelsiga  24875  measvun  24921  voliune  24943  volfiniune  24944  orvcval2  25109  dstfrvel  25124  ballotlemfc0  25143  ballotlemfcc  25144  ballotlemsv  25160  ballotlemsf1o  25164  sgnmulsgn  25200  relexpindlem  25599  rtrclreclem.trans  25606  dedekind  25644  dedekindle  25645  dfdm5  25857  dfrn5  25858  trpredpred  25963  poseq  25985  wsuclem  26033  nodense  26101  nocvxminlem  26102  nobnddown  26113  nofulllem4  26117  nofulllem5  26118  brpprod  26187  brsset  26191  brbigcup  26200  dffix2  26207  elfuns  26217  brimageg  26229  brdomaing  26237  brrangeg  26238  brimg  26239  brapply  26240  brsuccf  26243  funpartlem  26244  brrestrict  26251  dfrdg4  26252  axlowdim2  26356  axlowdim  26357  axcontlem2  26361  axcontlem3  26362  axcontlem4  26363  axcontlem7  26366  axcontlem9  26368  axcontlem10  26369  axcontlem11  26370  axcontlem12  26371  brofs  26396  btwncomim  26404  btwnintr  26410  btwnexch3  26411  btwnexch2  26414  brifs  26434  brcolinear2  26449  colineardim1  26452  brfs  26470  btwnconn1  26492  segcon2  26496  seglerflx  26503  seglemin  26504  btwnsegle  26508  colinbtwnle  26509  broutsideof2  26513  fvray  26532  lineunray  26538  lineelsb2  26539  linerflx1  26540  supaddc  26687  supadd  26688  ltflcei  26689  lxflflp1  26691  heicant  26695  mblfinlem1  26697  mblfinlem2  26698  itg2addnclem  26712  itg2addnclem3  26714  itg2addnc  26715  itg2gt0cn  26716  ibladdnclem  26717  iblmulc2nc  26726  itgabsnc  26730  bddiblnc  26731  ftc1anclem5  26740  ftc1anclem7  26742  ftc1anclem8  26743  ftc1anc  26744  trer  26775  elicc3  26776  finminlem  26777  nn0prpwlem  26781  nn0prpw  26782  indexdom  26892  filbcmb  26898  fdc  26905  prdsbnd  26958  heiborlem3  26978  rrnequiv  27000  prtlem10  27238  lzenom  27352  fphpdo  27400  irrapxlem4  27410  pellexlem6  27419  infmrgelbi  27463  pellfundre  27466  pellfundlb  27469  monotoddzz  27528  zindbi  27531  divalgmodcl  27580  jm2.27  27601  rmydioph  27607  rpnnen3lem  27624  fnwe2lem2  27648  aomclem8  27658  hbtlem5  27831  hbt  27833  pmtrval  27893  pmtrrn  27898  pmtrfrn  27899  phisum  28017  stoweidlem5  28248  stoweidlem20  28263  stoweidlem26  28269  stoweidlem28  28271  stoweidlem29  28272  stoweidlem34  28277  wallispilem3  28310  stirlinglem13  28329  funressnfv  28487  dfdfat2  28490  tz6.12-afv  28532  swrdccatid  28883  clwlkisclwwlklem2fv1  29128  clwwisshclwwlem1a  29155  cshwlemma1  29184  clwlkf1clwwlklem1  29214  isfrgra  29277  3vfriswmgra  29292  1to2vfriswmgra  29293  vdfrgra0  29309  vdgfrgra0  29310  numclwwlk5  29400  frgraregord013  29406  bnj23  30051  bnj1185  30133  bnj1152  30335  bnj1418  30377  lsatcveq0  30879  lsatcv1  30895  oposlem  31029  opnlen0  31035  lub0N  31036  glb0N  31040  omllaw  31090  cmtbr4N  31102  cvrval  31116  cvrnbtwn  31118  cvrnbtwn2  31122  cvrnbtwn3  31123  cvrcon3b  31124  cvrnbtwn4  31126  atcvreq0  31161  atnle  31164  atlatmstc  31166  cvlexch1  31175  glbconN  31223  hlsuprexch  31227  exatleN  31250  cvratlem  31267  atcvrj0  31274  atcvrj2b  31278  atlelt  31284  cvrat4  31289  3dim1lem5  31312  3dim2  31314  3dim3  31315  ps-2  31324  llni  31354  llnn0  31362  llnle  31364  lplni  31378  lplni2  31383  lplnle  31386  lplnn0N  31393  llncvrlpln  31404  2llnjN  31413  lvoli  31421  lvoli3  31423  lvoli2  31427  lvoln0N  31437  4at  31459  lplncvrlvol  31462  2lplnj  31466  dalemcea  31506  dalem3  31510  psubspi  31593  linepsubN  31598  elpmap  31604  pmapsub  31614  lnatexN  31625  cdlema1N  31637  cdlemb  31640  elpadd  31645  paddvaln0N  31647  paddasslem5  31670  llnexchb2lem  31714  llnexch2N  31716  islhp  31842  lhpat3  31892  4atexlemex2  31917  4atex  31922  4atex2-0aOLDN  31924  4atex2-0cOLDN  31926  lautle  31930  lautcvr  31938  lauteq  31941  ldilval  31959  ltrnu  31967  trlval2  32009  trlne  32031  cdleme0ex1N  32069  cdleme0nex  32136  cdleme18d  32141  cdlemednuN  32146  cdleme25b  32200  cdleme25cv  32204  cdleme27b  32214  cdleme29b  32221  cdleme31sn  32226  cdleme31fv  32236  cdleme31fv2  32239  cdlemefrs29bpre0  32242  cdlemefr29bpre0N  32252  cdlemefr29clN  32253  cdlemefr32fvaN  32255  cdlemefr32fva1  32256  cdlemefs29pre00N  32258  cdlemefs32sn1aw  32260  cdlemefs29bpre0N  32262  cdlemefs29bpre1N  32263  cdlemefs29cpre1N  32264  cdlemefs29clN  32265  cdlemefs32fvaN  32268  cdlemefs32fva1  32269  cdleme41sn3a  32279  cdleme32fva  32283  cdleme32e  32291  cdleme35f  32300  cdleme40v  32315  cdleme42b  32324  trlord  32415  cdlemg1cex  32434  diaval  32879  diaeldm  32883  diaelrnN  32892  cdlemm10N  32965  dibglbN  33013  dicval  33023  dicfnN  33030  dicvalrelN  33032  dihval  33079  dihlsscpre  33081  dihglblem3N  33142  dihmeetlem2N  33146  djhcvat42  33262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-5 1573  ax-17 1636  ax-9 1677  ax-8 1698  ax-6 1753  ax-7 1758  ax-11 1770  ax-12 1963  ax-ext 2460
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 940  df-tru 1334  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2466  df-cleq 2472  df-clel 2475  df-nfc 2604  df-rab 2757  df-v 3005  df-dif 3353  df-un 3355  df-in 3357  df-ss 3364  df-nul 3658  df-if 3810  df-sn 3894  df-pr 3895  df-op 3897  df-br 4294
  Copyright terms: Public domain W3C validator