Theorem breq1 4133

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ⟨cop 3712   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  breq12  4135  breq1i  4137  breq1d  4140  nbrne2  4150  brab1  4178  pocl  4448  swopolem  4450  swopo  4451  issod  4464  sowlin  4465  sotritrieq  4470  frirrg  4495  wetriext  4724  vtoclr  4823  brcog  4947  brcogw  4949  opelcnvg  4960  dfdmf  4974  eldmg  4976  dfrnf  5023  dfres2  5115  imasng  5152  coi1  5303  dffun6f  5390  funmo  5392  fun11  5448  fveq2  5695  funfveu  5708  sefvex  5716  nfunsn  5733  fvmptss2  5780  f1ompt  5859  fmptco  5874  dff13  5974  foeqcnvco  5996  isorel  6014  isocnv  6017  isotr  6022  isoini  6024  isopolem  6028  isosolem  6030  f1oiso  6032  f1oiso2  6033  caovordig  6255  caovordg  6257  caovord3d  6260  caovord  6261  caovord3  6263  caofrss  6334  caoftrn  6335  poxp  6468  brtpos2  6522  rntpos  6528  tpostpos  6535  ertr  6822  ecopovsym  6905  ecopovtrn  6906  ecopovsymg  6908  ecopovtrng  6909  th3qlem2  6912  isfi  7047  en0  7082  en1  7086  en1bg  7087  endisj  7122  xpcomco  7124  dom0  7138  ssenen  7152  nneneq  7158  domfiexmid  7182  findcard  7192  findcard2  7193  findcard2s  7194  isinfinf  7201  tridc  7204  fimax2gtrilemstep  7205  fimax2gtri  7206  fiintim  7238  fisseneq  7242  en1eqsnbi  7266  isbth  7284  supmoti  7334  eqsupti  7337  supubti  7340  suplubti  7341  supsnti  7346  isotilem  7347  isoti  7348  supisolem  7349  supisoex  7350  infminti  7368  isnumi  7528  cardval3ex  7531  oncardval  7532  cardonle  7533  en2prde  7540  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  papsym  7613  papcotr  7614  exmidapne  7627  nqtri3or  7764  ltsonq  7766  ltanqg  7768  ltmnqg  7769  ltexnqq  7776  subhalfnqq  7782  ltbtwnnqq  7783  archnqq  7785  nqnq0pi  7806  prcdnql  7852  prcunqu  7853  prnmaxl  7856  genpcuu  7888  genprndl  7889  genprndu  7890  nqprm  7910  nqprrnd  7911  nqprdisj  7912  nqprloc  7913  nqpru  7920  addnqprlemrl  7925  addnqprlemfl  7927  addnqprlemfu  7928  prmuloc2  7935  mulnqprlemrl  7941  mulnqprlemfl  7943  mulnqprlemfu  7944  1idprl  7958  ltnqpr  7961  ltnqpri  7962  prplnqu  7988  recexprlemell  7990  recexprlemm  7992  recexprlemdisj  7998  recexprlemloc  7999  recexprlem1ssu  8002  recexprlemss1l  8003  aptiprlemu  8008  archpr  8011  cauappcvgprlemm  8013  cauappcvgprlemladdfl  8023  cauappcvgprlem2  8028  cauappcvgpr  8030  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemcl  8044  caucvgprlem2  8048  caucvgpr  8050  caucvgprprlemelu  8054  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnbj  8061  caucvgprprlemmu  8063  caucvgprprlemopu  8067  caucvgprprlemexbt  8074  caucvgprprlemaddq  8076  caucvgprprlem1  8077  caucvgprprlem2  8078  caucvgprpr  8080  suplocexprlemmu  8086  suplocexprlemloc  8089  suplocexpr  8093  lttrsr  8130  ltsosr  8132  1ne0sr  8134  ltasrg  8138  aptisr  8147  mulextsr1  8149  archsr  8150  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  caucvgsr  8170  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  axpre-ltwlin  8251  axpre-lttrn  8252  axpre-apti  8253  axpre-ltadd  8254  axpre-mulext  8256  axcaucvglemcau  8266  axcaucvglemres  8267  axcaucvg  8268  axpre-suploclemres  8269  axpre-suploc  8270  ltxrlt  8392  lttri3  8406  ltordlem  8812  lt0ne0d  8843  reapti  8910  apreim  8934  apsscn  8978  recexap  8984  lbreu  9278  lble  9280  suprleubex  9287  sup3exmid  9290  nnsub  9346  nominpos  9548  nn0n0n1ge2b  9730  zextle  9742  fzind  9766  btwnz  9770  uzval  9933  supinfneg  10005  infsupneg  10006  infregelbex  10008  ublbneg  10023  lbzbi  10026  qreccl  10052  xrltnsym  10206  xrlttr  10208  xrltso  10209  xrlttri3  10210  nltpnft  10227  npnflt  10228  xrrebnd  10232  xltnegi  10248  xnn0lenn0nn0  10278  xsubge0  10294  xlesubadd  10296  xleaddadd  10300  ixxval  10309  elixx1  10310  elioo2  10334  iccid  10338  fzval  10424  elfz1  10427  zsupcllemstep  10673  suprzubdc  10682  zsupssdc  10684  qtri3or  10686  exbtwnzlemstep  10693  exbtwnzlemshrink  10694  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2zlemshrink  10699  rebtwn2z  10700  qbtwnre  10702  qbtwnxr  10703  flval  10718  flqlelt  10723  flaplelt  10724  flqbi  10740  flqeqceilz  10770  modqid2  10803  seq3f1olemqsum  10965  seq3f1oleml  10968  seq3f1o  10969  seqf1oglem2  10972  expcl2lemap  11003  expclzaplem  11015  expclzap  11016  expap0i  11023  nn0ltexp2  11163  hashinfuni  11232  hashennnuni  11234  hashunlem  11260  zfz1isolemiso  11307  zfz1isolem1  11308  zfz1iso  11309  absle  11872  maxleast  11996  rexanre  12003  rexico  12004  fimaxre2  12010  minmax  12014  xrmaxltsup  12043  xrminmax  12050  climshft  12089  reccn2ap  12098  summodclem3  12166  summodclem2a  12167  summodc  12169  zsumdc  12170  fsum3  12173  fsum3cvg3  12182  fsumcl2lem  12184  fsumadd  12192  sumsnf  12195  fsummulc2  12234  isumlessdc  12282  cvgratz  12318  mertenslemi1  12321  ntrivcvgap0  12335  prodmodclem3  12361  prodmodclem2a  12362  prodmodc  12364  zproddc  12365  fprodseq  12369  fprodntrivap  12370  fprodmul  12377  prodsnf  12378  absdvdsb  12595  zdvdsdc  12598  dvdsabseq  12633  dvdsdivcl  12636  dvdsext  12641  divalglemnn  12704  divalglemeunn  12707  divalglemeuneg  12709  divalgmod  12713  ndvdssub  12716  gcdsupex  12753  gcdsupcl  12754  gcddvds  12759  dvdslegcd  12760  bezoutlemmain  12794  bezoutlemex  12797  bezoutlemzz  12798  bezoutlemmo  12802  bezoutlemeu  12803  bezoutlemle  12804  bezoutlemsup  12805  dfgcd3  12806  dfgcd2  12810  gcdzeq  12818  dvdssq  12827  nnwodc  12832  uzwodc  12833  nnwofdc  12834  nn0seqcvgd  12838  algcvgblem  12846  lcmval  12860  lcmdvds  12876  lcmgcdeq  12880  coprmgcdb  12885  ncoprmgcdne1b  12886  coprmdvds1  12888  1nprm  12911  1idssfct  12912  isprm2lem  12913  isprm2  12914  dvdsprime  12919  nprm  12920  3prm  12925  dvdsprm  12935  exprmfct  12936  isprm5lem  12939  isprm5  12940  coprm  12942  sqrt2irr  12960  dvdsfi  13040  phisum  13042  odzval  13043  pythagtriplem4  13070  pc2dvds  13132  pcprmpw2  13135  pcprmpw  13136  dvdsprmpweqle  13139  oddprmdvds  13156  prmpwdvds  13157  pockthg  13159  1arith  13169  prmlem0  13243  prmlem1a  13244  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemsv  13305  ballotfilemsf1o  13309  ballotfi  13334  exmidunben  13369  nninfdclemcl  13391  nninfdclemp1  13393  nninfdc  13396  imasaddfnlemg  13688  ringunitsap0  14678  drnguiap  14693  cnfldui  15008  znleval  15072  psrbagconcl  15148  rhmpsrfilem2  15157  ssblex  15623  comet  15691  bdmopn  15696  reopnap  15738  divcnap  15757  cdivcncfap  15796  cnopnap  15803  divcncfap  15806  maxcncf  15807  mincncf  15808  dedekindeulemuub  15809  dedekindeulemloc  15811  dedekindeulemlu  15813  dedekindeulemeu  15814  dedekindeu  15815  suplociccreex  15816  dedekindicclemuub  15818  dedekindicclemloc  15820  dedekindicclemlu  15822  dedekindicclemeu  15823  dedekindicclemicc  15824  dedekindicc  15825  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemloc  15833  ivthinc  15835  ivthreinc  15837  dich0  15844  ivthdich  15845  limcdifap  15854  limcimolemlt  15856  limccoap  15870  dvlemap  15872  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvrecap  15905  dveflem  15918  logltb  16068  2irrexpqap  16175  prmdvdsfi  16204  sgmnncl  16218  dvdsppwf1o  16244  mpodvdsmulf1o  16245  perfectlem2  16261  bcmono  16265  bpos1lem  16270  bposlem9  16280  lgsmod  16311  lgsne0  16323  gausslemma2dlem4  16349  2sqlem6  16405  2sqlem8  16408  2sqlem10  16410  upgrm  16507  upgr1or2  16508  umgredg2en  16516  umgrbien  16517  upgr1elem1  16527  umgr1een  16532  edgupgren  16548  edgumgren  16549  umgredgnlp  16559  edgusgren  16570  usgruspgrben  16593  usgr1e  16648  subumgredg2en  16678  subupgr  16680  wlkvtxiedg  16752  wlkvtxiedgg  16753  istrl  16792  iseupth  16854  eupth2fi  16886  konigsberglem1  16895  lealltlt1  16917  pw1nct  17199  sbthom  17237  rirrdisj  17251  trilpo  17259  trirec0  17260  reap0  17275  cndcap  17276  dcapnconst  17278  neapmkv  17285  neap0mkv  17286  ltlenmkv  17287