Theorem breq1 4089

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
breq1	⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Proof of Theorem breq1

Step	Hyp	Ref	Expression
1		opeq1 3860	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	eleq1d 2298	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3		df-br 4087	. 2 ⊢ (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4		df-br 4087	. 2 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ⟨cop 3670   class class class wbr 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  breq12  4091  breq1i  4093  breq1d  4096  nbrne2  4106  brab1  4134  pocl  4398  swopolem  4400  swopo  4401  issod  4414  sowlin  4415  sotritrieq  4420  frirrg  4445  wetriext  4673  vtoclr  4772  brcog  4895  brcogw  4897  opelcnvg  4908  dfdmf  4922  eldmg  4924  dfrnf  4971  dfres2  5063  imasng  5099  coi1  5250  dffun6f  5337  funmo  5339  fun11  5394  fveq2  5635  funfveu  5648  sefvex  5656  nfunsn  5672  fvmptss2  5717  f1ompt  5794  fmptco  5809  dff13  5904  foeqcnvco  5926  isorel  5944  isocnv  5947  isotr  5952  isoini  5954  isopolem  5958  isosolem  5960  f1oiso  5962  f1oiso2  5963  caovordig  6183  caovordg  6185  caovord3d  6188  caovord  6189  caovord3  6191  caofrss  6262  caoftrn  6263  poxp  6392  brtpos2  6412  rntpos  6418  tpostpos  6425  ertr  6712  ecopovsym  6795  ecopovtrn  6796  ecopovsymg  6798  ecopovtrng  6799  th3qlem2  6802  isfi  6929  en0  6964  en1  6968  en1bg  6969  endisj  7003  xpcomco  7005  dom0  7019  ssenen  7032  nneneq  7038  domfiexmid  7060  findcard  7070  findcard2  7071  findcard2s  7072  isinfinf  7079  tridc  7082  fimax2gtrilemstep  7083  fimax2gtri  7084  fiintim  7116  fisseneq  7119  en1eqsnbi  7139  isbth  7157  supmoti  7183  eqsupti  7186  supubti  7189  suplubti  7190  supsnti  7195  isotilem  7196  isoti  7197  supisolem  7198  supisoex  7199  infminti  7217  isnumi  7377  cardval3ex  7380  oncardval  7381  cardonle  7382  en2prde  7389  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidapne  7469  nqtri3or  7606  ltsonq  7608  ltanqg  7610  ltmnqg  7611  ltexnqq  7618  subhalfnqq  7624  ltbtwnnqq  7625  archnqq  7627  nqnq0pi  7648  prcdnql  7694  prcunqu  7695  prnmaxl  7698  genpcuu  7730  genprndl  7731  genprndu  7732  nqprm  7752  nqprrnd  7753  nqprdisj  7754  nqprloc  7755  nqpru  7762  addnqprlemrl  7767  addnqprlemfl  7769  addnqprlemfu  7770  prmuloc2  7777  mulnqprlemrl  7783  mulnqprlemfl  7785  mulnqprlemfu  7786  1idprl  7800  ltnqpr  7803  ltnqpri  7804  prplnqu  7830  recexprlemell  7832  recexprlemm  7834  recexprlemdisj  7840  recexprlemloc  7841  recexprlem1ssu  7844  recexprlemss1l  7845  aptiprlemu  7850  archpr  7853  cauappcvgprlemm  7855  cauappcvgprlemladdfl  7865  cauappcvgprlem2  7870  cauappcvgpr  7872  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemcl  7886  caucvgprlem2  7890  caucvgpr  7892  caucvgprprlemelu  7896  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemnbj  7903  caucvgprprlemmu  7905  caucvgprprlemopu  7909  caucvgprprlemexbt  7916  caucvgprprlemaddq  7918  caucvgprprlem1  7919  caucvgprprlem2  7920  caucvgprpr  7922  suplocexprlemmu  7928  suplocexprlemloc  7931  suplocexpr  7935  lttrsr  7972  ltsosr  7974  1ne0sr  7976  ltasrg  7980  aptisr  7989  mulextsr1  7991  archsr  7992  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  caucvgsr  8012  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  axpre-ltwlin  8093  axpre-lttrn  8094  axpre-apti  8095  axpre-ltadd  8096  axpre-mulext  8098  axcaucvglemcau  8108  axcaucvglemres  8109  axcaucvg  8110  axpre-suploclemres  8111  axpre-suploc  8112  ltxrlt  8235  lttri3  8249  ltordlem  8652  lt0ne0d  8683  reapti  8749  apreim  8773  apsscn  8817  recexap  8823  lbreu  9115  lble  9117  suprleubex  9124  sup3exmid  9127  nnsub  9172  nominpos  9372  nn0n0n1ge2b  9549  zextle  9561  fzind  9585  btwnz  9589  uzval  9747  supinfneg  9819  infsupneg  9820  infregelbex  9822  ublbneg  9837  lbzbi  9840  qreccl  9866  xrltnsym  10018  xrlttr  10020  xrltso  10021  xrlttri3  10022  nltpnft  10039  npnflt  10040  xrrebnd  10044  xltnegi  10060  xnn0lenn0nn0  10090  xsubge0  10106  xlesubadd  10108  xleaddadd  10112  ixxval  10121  elixx1  10122  elioo2  10146  iccid  10150  fzval  10235  elfz1  10238  zsupcllemstep  10479  suprzubdc  10486  zsupssdc  10488  qtri3or  10490  exbtwnzlemstep  10497  exbtwnzlemshrink  10498  exbtwnzlemex  10499  exbtwnz  10500  rebtwn2zlemstep  10502  rebtwn2zlemshrink  10503  rebtwn2z  10504  qbtwnre  10506  qbtwnxr  10507  flval  10522  flqlelt  10526  flqbi  10540  flqeqceilz  10570  modqid2  10603  seq3f1olemqsum  10765  seq3f1oleml  10768  seq3f1o  10769  seqf1oglem2  10772  expcl2lemap  10803  expclzaplem  10815  expclzap  10816  expap0i  10823  nn0ltexp2  10961  hashinfuni  11029  hashennnuni  11031  hashunlem  11057  zfz1isolemiso  11093  zfz1isolem1  11094  zfz1iso  11095  absle  11640  maxleast  11764  rexanre  11771  rexico  11772  fimaxre2  11778  minmax  11781  xrmaxltsup  11809  xrminmax  11816  climshft  11855  reccn2ap  11864  summodclem3  11931  summodclem2a  11932  summodc  11934  zsumdc  11935  fsum3  11938  fsum3cvg3  11947  fsumcl2lem  11949  fsumadd  11957  sumsnf  11960  fsummulc2  11999  isumlessdc  12047  cvgratz  12083  mertenslemi1  12086  ntrivcvgap0  12100  prodmodclem3  12126  prodmodclem2a  12127  prodmodc  12129  zproddc  12130  fprodseq  12134  fprodntrivap  12135  fprodmul  12142  prodsnf  12143  absdvdsb  12360  zdvdsdc  12363  dvdsabseq  12398  dvdsdivcl  12401  dvdsext  12406  divalglemnn  12469  divalglemeunn  12472  divalglemeuneg  12474  divalgmod  12478  ndvdssub  12481  gcdsupex  12518  gcdsupcl  12519  gcddvds  12524  dvdslegcd  12525  bezoutlemmain  12559  bezoutlemex  12562  bezoutlemzz  12563  bezoutlemmo  12567  bezoutlemeu  12568  bezoutlemle  12569  bezoutlemsup  12570  dfgcd3  12571  dfgcd2  12575  gcdzeq  12583  dvdssq  12592  nnwodc  12597  uzwodc  12598  nnwofdc  12599  nn0seqcvgd  12603  algcvgblem  12611  lcmval  12625  lcmdvds  12641  lcmgcdeq  12645  coprmgcdb  12650  ncoprmgcdne1b  12651  coprmdvds1  12653  1nprm  12676  1idssfct  12677  isprm2lem  12678  isprm2  12679  dvdsprime  12684  nprm  12685  3prm  12690  dvdsprm  12699  exprmfct  12700  isprm5lem  12703  isprm5  12704  coprm  12706  sqrt2irr  12724  dvdsfi  12801  phisum  12803  odzval  12804  pythagtriplem4  12831  pc2dvds  12893  pcprmpw2  12896  pcprmpw  12897  dvdsprmpweqle  12900  oddprmdvds  12917  prmpwdvds  12918  pockthg  12920  1arith  12930  exmidunben  13037  nninfdclemcl  13059  nninfdclemp1  13061  nninfdc  13064  imasaddfnlemg  13387  cnfldui  14593  znleval  14657  ssblex  15145  comet  15213  bdmopn  15218  reopnap  15260  divcnap  15279  cdivcncfap  15318  cnopnap  15325  divcncfap  15328  maxcncf  15329  mincncf  15330  dedekindeulemuub  15331  dedekindeulemloc  15333  dedekindeulemlu  15335  dedekindeulemeu  15336  dedekindeu  15337  suplociccreex  15338  dedekindicclemuub  15340  dedekindicclemloc  15342  dedekindicclemlu  15344  dedekindicclemeu  15345  dedekindicclemicc  15346  dedekindicc  15347  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemloc  15355  ivthinc  15357  ivthreinc  15359  dich0  15366  ivthdich  15367  limcdifap  15376  limcimolemlt  15378  limccoap  15392  dvlemap  15394  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvcjbr  15422  dvrecap  15427  dveflem  15440  logltb  15588  2irrexpqap  15692  sgmnncl  15702  dvdsppwf1o  15703  mpodvdsmulf1o  15704  perfectlem2  15714  lgsmod  15745  lgsne0  15757  gausslemma2dlem4  15783  2sqlem6  15839  2sqlem8  15842  2sqlem10  15844  upgrm  15941  upgr1or2  15942  umgredg2en  15950  umgrbien  15951  upgr1elem1  15961  edgupgren  15980  edgumgren  15981  umgredgnlp  15991  edgusgren  16002  usgruspgrben  16025  usgr1e  16080  wlkvtxiedg  16142  wlkvtxiedgg  16143  istrl  16180  iseupth  16242  pw1nct  16540  sbthom  16566  trilpo  16583  trirec0  16584  reap0  16598  cndcap  16599  dcapnconst  16601  neapmkv  16608  neap0mkv  16609  ltlenmkv  16610