Theorem breq1 4036

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 3808	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	eleq1d 2265	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3		df-br 4034	. 2 ⊢ (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4		df-br 4034	. 2 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2167  ⟨cop 3625   class class class wbr 4033

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034

This theorem is referenced by:  breq12  4038  breq1i  4040  breq1d  4043  nbrne2  4053  brab1  4080  pocl  4338  swopolem  4340  swopo  4341  issod  4354  sowlin  4355  sotritrieq  4360  frirrg  4385  wetriext  4613  vtoclr  4711  brcog  4833  brcogw  4835  opelcnvg  4846  dfdmf  4859  eldmg  4861  dfrnf  4907  dfres2  4998  imasng  5034  coi1  5185  dffun6f  5271  funmo  5273  fun11  5325  fveq2  5558  funfveu  5571  sefvex  5579  nfunsn  5593  fvmptss2  5636  f1ompt  5713  fmptco  5728  dff13  5815  foeqcnvco  5837  isorel  5855  isocnv  5858  isotr  5863  isoini  5865  isopolem  5869  isosolem  5871  f1oiso  5873  f1oiso2  5874  caovordig  6089  caovordg  6091  caovord3d  6094  caovord  6095  caovord3  6097  caofrss  6162  caoftrn  6163  poxp  6290  brtpos2  6309  rntpos  6315  tpostpos  6322  ertr  6607  ecopovsym  6690  ecopovtrn  6691  ecopovsymg  6693  ecopovtrng  6694  th3qlem2  6697  isfi  6820  en0  6854  en1  6858  en1bg  6859  endisj  6883  xpcomco  6885  dom0  6899  ssenen  6912  nneneq  6918  domfiexmid  6939  findcard  6949  findcard2  6950  findcard2s  6951  isinfinf  6958  tridc  6960  fimax2gtrilemstep  6961  fimax2gtri  6962  fiintim  6992  fisseneq  6995  en1eqsnbi  7015  isbth  7033  supmoti  7059  eqsupti  7062  supubti  7065  suplubti  7066  supsnti  7071  isotilem  7072  isoti  7073  supisolem  7074  supisoex  7075  infminti  7093  isnumi  7249  cardval3ex  7252  oncardval  7253  cardonle  7254  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidapne  7327  nqtri3or  7463  ltsonq  7465  ltanqg  7467  ltmnqg  7468  ltexnqq  7475  subhalfnqq  7481  ltbtwnnqq  7482  archnqq  7484  nqnq0pi  7505  prcdnql  7551  prcunqu  7552  prnmaxl  7555  genpcuu  7587  genprndl  7588  genprndu  7589  nqprm  7609  nqprrnd  7610  nqprdisj  7611  nqprloc  7612  nqpru  7619  addnqprlemrl  7624  addnqprlemfl  7626  addnqprlemfu  7627  prmuloc2  7634  mulnqprlemrl  7640  mulnqprlemfl  7642  mulnqprlemfu  7643  1idprl  7657  ltnqpr  7660  ltnqpri  7661  prplnqu  7687  recexprlemell  7689  recexprlemm  7691  recexprlemdisj  7697  recexprlemloc  7698  recexprlem1ssu  7701  recexprlemss1l  7702  aptiprlemu  7707  archpr  7710  cauappcvgprlemm  7712  cauappcvgprlemladdfl  7722  cauappcvgprlem2  7727  cauappcvgpr  7729  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemcl  7743  caucvgprlem2  7747  caucvgpr  7749  caucvgprprlemelu  7753  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemnbj  7760  caucvgprprlemmu  7762  caucvgprprlemopu  7766  caucvgprprlemexbt  7773  caucvgprprlemaddq  7775  caucvgprprlem1  7776  caucvgprprlem2  7777  caucvgprpr  7779  suplocexprlemmu  7785  suplocexprlemloc  7788  suplocexpr  7792  lttrsr  7829  ltsosr  7831  1ne0sr  7833  ltasrg  7837  aptisr  7846  mulextsr1  7848  archsr  7849  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  caucvgsr  7869  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  axpre-ltwlin  7950  axpre-lttrn  7951  axpre-apti  7952  axpre-ltadd  7953  axpre-mulext  7955  axcaucvglemcau  7965  axcaucvglemres  7966  axcaucvg  7967  axpre-suploclemres  7968  axpre-suploc  7969  ltxrlt  8092  lttri3  8106  ltordlem  8509  lt0ne0d  8540  reapti  8606  apreim  8630  apsscn  8674  recexap  8680  lbreu  8972  lble  8974  suprleubex  8981  sup3exmid  8984  nnsub  9029  nominpos  9229  nn0n0n1ge2b  9405  zextle  9417  fzind  9441  btwnz  9445  uzval  9603  supinfneg  9669  infsupneg  9670  infregelbex  9672  ublbneg  9687  lbzbi  9690  qreccl  9716  xrltnsym  9868  xrlttr  9870  xrltso  9871  xrlttri3  9872  nltpnft  9889  npnflt  9890  xrrebnd  9894  xltnegi  9910  xnn0lenn0nn0  9940  xsubge0  9956  xlesubadd  9958  xleaddadd  9962  ixxval  9971  elixx1  9972  elioo2  9996  iccid  10000  fzval  10085  elfz1  10088  zsupcllemstep  10319  suprzubdc  10326  zsupssdc  10328  qtri3or  10330  exbtwnzlemstep  10337  exbtwnzlemshrink  10338  exbtwnzlemex  10339  exbtwnz  10340  rebtwn2zlemstep  10342  rebtwn2zlemshrink  10343  rebtwn2z  10344  qbtwnre  10346  qbtwnxr  10347  flval  10362  flqlelt  10366  flqbi  10380  flqeqceilz  10410  modqid2  10443  seq3f1olemqsum  10605  seq3f1oleml  10608  seq3f1o  10609  seqf1oglem2  10612  expcl2lemap  10643  expclzaplem  10655  expclzap  10656  expap0i  10663  nn0ltexp2  10801  hashinfuni  10869  hashennnuni  10871  hashunlem  10896  zfz1isolemiso  10931  zfz1isolem1  10932  zfz1iso  10933  absle  11254  maxleast  11378  rexanre  11385  rexico  11386  fimaxre2  11392  minmax  11395  xrmaxltsup  11423  xrminmax  11430  climshft  11469  reccn2ap  11478  summodclem3  11545  summodclem2a  11546  summodc  11548  zsumdc  11549  fsum3  11552  fsum3cvg3  11561  fsumcl2lem  11563  fsumadd  11571  sumsnf  11574  fsummulc2  11613  isumlessdc  11661  cvgratz  11697  mertenslemi1  11700  ntrivcvgap0  11714  prodmodclem3  11740  prodmodclem2a  11741  prodmodc  11743  zproddc  11744  fprodseq  11748  fprodntrivap  11749  fprodmul  11756  prodsnf  11757  absdvdsb  11974  zdvdsdc  11977  dvdsabseq  12012  dvdsdivcl  12015  dvdsext  12020  divalglemnn  12083  divalglemeunn  12086  divalglemeuneg  12088  divalgmod  12092  ndvdssub  12095  gcdsupex  12124  gcdsupcl  12125  gcddvds  12130  dvdslegcd  12131  bezoutlemmain  12165  bezoutlemex  12168  bezoutlemzz  12169  bezoutlemmo  12173  bezoutlemeu  12174  bezoutlemle  12175  bezoutlemsup  12176  dfgcd3  12177  dfgcd2  12181  gcdzeq  12189  dvdssq  12198  nnwodc  12203  uzwodc  12204  nnwofdc  12205  nn0seqcvgd  12209  algcvgblem  12217  lcmval  12231  lcmdvds  12247  lcmgcdeq  12251  coprmgcdb  12256  ncoprmgcdne1b  12257  coprmdvds1  12259  1nprm  12282  1idssfct  12283  isprm2lem  12284  isprm2  12285  dvdsprime  12290  nprm  12291  3prm  12296  dvdsprm  12305  exprmfct  12306  isprm5lem  12309  isprm5  12310  coprm  12312  sqrt2irr  12330  dvdsfi  12407  phisum  12409  odzval  12410  pythagtriplem4  12437  pc2dvds  12499  pcprmpw2  12502  pcprmpw  12503  dvdsprmpweqle  12506  oddprmdvds  12523  prmpwdvds  12524  pockthg  12526  1arith  12536  exmidunben  12643  nninfdclemcl  12665  nninfdclemp1  12667  nninfdc  12670  imasaddfnlemg  12957  cnfldui  14145  znleval  14209  ssblex  14667  comet  14735  bdmopn  14740  reopnap  14782  divcnap  14801  cdivcncfap  14840  cnopnap  14847  divcncfap  14850  maxcncf  14851  mincncf  14852  dedekindeulemuub  14853  dedekindeulemloc  14855  dedekindeulemlu  14857  dedekindeulemeu  14858  dedekindeu  14859  suplociccreex  14860  dedekindicclemuub  14862  dedekindicclemloc  14864  dedekindicclemlu  14866  dedekindicclemeu  14867  dedekindicclemicc  14868  dedekindicc  14869  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemloc  14877  ivthinc  14879  ivthreinc  14881  dich0  14888  ivthdich  14889  limcdifap  14898  limcimolemlt  14900  limccoap  14914  dvlemap  14916  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvrecap  14949  dveflem  14962  logltb  15110  2irrexpqap  15214  sgmnncl  15224  dvdsppwf1o  15225  mpodvdsmulf1o  15226  perfectlem2  15236  lgsmod  15267  lgsne0  15279  gausslemma2dlem4  15305  2sqlem6  15361  2sqlem8  15364  2sqlem10  15366  pw1nct  15647  sbthom  15670  trilpo  15687  trirec0  15688  reap0  15702  cndcap  15703  dcapnconst  15705  neapmkv  15712  neap0mkv  15713  ltlenmkv  15714