Theorem breq1 4087

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

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

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 4085

This theorem is referenced by:  breq12  4089  breq1i  4091  breq1d  4094  nbrne2  4104  brab1  4132  pocl  4396  swopolem  4398  swopo  4399  issod  4412  sowlin  4413  sotritrieq  4418  frirrg  4443  wetriext  4671  vtoclr  4770  brcog  4893  brcogw  4895  opelcnvg  4906  dfdmf  4920  eldmg  4922  dfrnf  4969  dfres2  5061  imasng  5097  coi1  5248  dffun6f  5335  funmo  5337  fun11  5392  fveq2  5633  funfveu  5646  sefvex  5654  nfunsn  5670  fvmptss2  5715  f1ompt  5792  fmptco  5807  dff13  5902  foeqcnvco  5924  isorel  5942  isocnv  5945  isotr  5950  isoini  5952  isopolem  5956  isosolem  5958  f1oiso  5960  f1oiso2  5961  caovordig  6181  caovordg  6183  caovord3d  6186  caovord  6187  caovord3  6189  caofrss  6260  caoftrn  6261  poxp  6390  brtpos2  6410  rntpos  6416  tpostpos  6423  ertr  6710  ecopovsym  6793  ecopovtrn  6794  ecopovsymg  6796  ecopovtrng  6797  th3qlem2  6800  isfi  6927  en0  6962  en1  6966  en1bg  6967  endisj  7001  xpcomco  7003  dom0  7017  ssenen  7030  nneneq  7036  domfiexmid  7058  findcard  7068  findcard2  7069  findcard2s  7070  isinfinf  7077  tridc  7080  fimax2gtrilemstep  7081  fimax2gtri  7082  fiintim  7114  fisseneq  7117  en1eqsnbi  7137  isbth  7155  supmoti  7181  eqsupti  7184  supubti  7187  suplubti  7188  supsnti  7193  isotilem  7194  isoti  7195  supisolem  7196  supisoex  7197  infminti  7215  isnumi  7375  cardval3ex  7378  oncardval  7379  cardonle  7380  en2prde  7387  exmidfodomrlemr  7401  exmidfodomrlemrALT  7402  exmidapne  7467  nqtri3or  7604  ltsonq  7606  ltanqg  7608  ltmnqg  7609  ltexnqq  7616  subhalfnqq  7622  ltbtwnnqq  7623  archnqq  7625  nqnq0pi  7646  prcdnql  7692  prcunqu  7693  prnmaxl  7696  genpcuu  7728  genprndl  7729  genprndu  7730  nqprm  7750  nqprrnd  7751  nqprdisj  7752  nqprloc  7753  nqpru  7760  addnqprlemrl  7765  addnqprlemfl  7767  addnqprlemfu  7768  prmuloc2  7775  mulnqprlemrl  7781  mulnqprlemfl  7783  mulnqprlemfu  7784  1idprl  7798  ltnqpr  7801  ltnqpri  7802  prplnqu  7828  recexprlemell  7830  recexprlemm  7832  recexprlemdisj  7838  recexprlemloc  7839  recexprlem1ssu  7842  recexprlemss1l  7843  aptiprlemu  7848  archpr  7851  cauappcvgprlemm  7853  cauappcvgprlemladdfl  7863  cauappcvgprlem2  7868  cauappcvgpr  7870  caucvgprlemnkj  7874  caucvgprlemnbj  7875  caucvgprlemcl  7884  caucvgprlem2  7888  caucvgpr  7890  caucvgprprlemelu  7894  caucvgprprlemcbv  7895  caucvgprprlemval  7896  caucvgprprlemnbj  7901  caucvgprprlemmu  7903  caucvgprprlemopu  7907  caucvgprprlemexbt  7914  caucvgprprlemaddq  7916  caucvgprprlem1  7917  caucvgprprlem2  7918  caucvgprpr  7920  suplocexprlemmu  7926  suplocexprlemloc  7929  suplocexpr  7933  lttrsr  7970  ltsosr  7972  1ne0sr  7974  ltasrg  7978  aptisr  7987  mulextsr1  7989  archsr  7990  caucvgsrlemgt1  8003  caucvgsrlemoffres  8008  caucvgsr  8010  suplocsrlemb  8014  suplocsrlempr  8015  suplocsrlem  8016  axpre-ltwlin  8091  axpre-lttrn  8092  axpre-apti  8093  axpre-ltadd  8094  axpre-mulext  8096  axcaucvglemcau  8106  axcaucvglemres  8107  axcaucvg  8108  axpre-suploclemres  8109  axpre-suploc  8110  ltxrlt  8233  lttri3  8247  ltordlem  8650  lt0ne0d  8681  reapti  8747  apreim  8771  apsscn  8815  recexap  8821  lbreu  9113  lble  9115  suprleubex  9122  sup3exmid  9125  nnsub  9170  nominpos  9370  nn0n0n1ge2b  9547  zextle  9559  fzind  9583  btwnz  9587  uzval  9745  supinfneg  9817  infsupneg  9818  infregelbex  9820  ublbneg  9835  lbzbi  9838  qreccl  9864  xrltnsym  10016  xrlttr  10018  xrltso  10019  xrlttri3  10020  nltpnft  10037  npnflt  10038  xrrebnd  10042  xltnegi  10058  xnn0lenn0nn0  10088  xsubge0  10104  xlesubadd  10106  xleaddadd  10110  ixxval  10119  elixx1  10120  elioo2  10144  iccid  10148  fzval  10233  elfz1  10236  zsupcllemstep  10477  suprzubdc  10484  zsupssdc  10486  qtri3or  10488  exbtwnzlemstep  10495  exbtwnzlemshrink  10496  exbtwnzlemex  10497  exbtwnz  10498  rebtwn2zlemstep  10500  rebtwn2zlemshrink  10501  rebtwn2z  10502  qbtwnre  10504  qbtwnxr  10505  flval  10520  flqlelt  10524  flqbi  10538  flqeqceilz  10568  modqid2  10601  seq3f1olemqsum  10763  seq3f1oleml  10766  seq3f1o  10767  seqf1oglem2  10770  expcl2lemap  10801  expclzaplem  10813  expclzap  10814  expap0i  10821  nn0ltexp2  10959  hashinfuni  11027  hashennnuni  11029  hashunlem  11054  zfz1isolemiso  11090  zfz1isolem1  11091  zfz1iso  11092  absle  11637  maxleast  11761  rexanre  11768  rexico  11769  fimaxre2  11775  minmax  11778  xrmaxltsup  11806  xrminmax  11813  climshft  11852  reccn2ap  11861  summodclem3  11928  summodclem2a  11929  summodc  11931  zsumdc  11932  fsum3  11935  fsum3cvg3  11944  fsumcl2lem  11946  fsumadd  11954  sumsnf  11957  fsummulc2  11996  isumlessdc  12044  cvgratz  12080  mertenslemi1  12083  ntrivcvgap0  12097  prodmodclem3  12123  prodmodclem2a  12124  prodmodc  12126  zproddc  12127  fprodseq  12131  fprodntrivap  12132  fprodmul  12139  prodsnf  12140  absdvdsb  12357  zdvdsdc  12360  dvdsabseq  12395  dvdsdivcl  12398  dvdsext  12403  divalglemnn  12466  divalglemeunn  12469  divalglemeuneg  12471  divalgmod  12475  ndvdssub  12478  gcdsupex  12515  gcdsupcl  12516  gcddvds  12521  dvdslegcd  12522  bezoutlemmain  12556  bezoutlemex  12559  bezoutlemzz  12560  bezoutlemmo  12564  bezoutlemeu  12565  bezoutlemle  12566  bezoutlemsup  12567  dfgcd3  12568  dfgcd2  12572  gcdzeq  12580  dvdssq  12589  nnwodc  12594  uzwodc  12595  nnwofdc  12596  nn0seqcvgd  12600  algcvgblem  12608  lcmval  12622  lcmdvds  12638  lcmgcdeq  12642  coprmgcdb  12647  ncoprmgcdne1b  12648  coprmdvds1  12650  1nprm  12673  1idssfct  12674  isprm2lem  12675  isprm2  12676  dvdsprime  12681  nprm  12682  3prm  12687  dvdsprm  12696  exprmfct  12697  isprm5lem  12700  isprm5  12701  coprm  12703  sqrt2irr  12721  dvdsfi  12798  phisum  12800  odzval  12801  pythagtriplem4  12828  pc2dvds  12890  pcprmpw2  12893  pcprmpw  12894  dvdsprmpweqle  12897  oddprmdvds  12914  prmpwdvds  12915  pockthg  12917  1arith  12927  exmidunben  13034  nninfdclemcl  13056  nninfdclemp1  13058  nninfdc  13061  imasaddfnlemg  13384  cnfldui  14590  znleval  14654  ssblex  15142  comet  15210  bdmopn  15215  reopnap  15257  divcnap  15276  cdivcncfap  15315  cnopnap  15322  divcncfap  15325  maxcncf  15326  mincncf  15327  dedekindeulemuub  15328  dedekindeulemloc  15330  dedekindeulemlu  15332  dedekindeulemeu  15333  dedekindeu  15334  suplociccreex  15335  dedekindicclemuub  15337  dedekindicclemloc  15339  dedekindicclemlu  15341  dedekindicclemeu  15342  dedekindicclemicc  15343  dedekindicc  15344  ivthinclemlopn  15347  ivthinclemlr  15348  ivthinclemuopn  15349  ivthinclemur  15350  ivthinclemloc  15352  ivthinc  15354  ivthreinc  15356  dich0  15363  ivthdich  15364  limcdifap  15373  limcimolemlt  15375  limccoap  15389  dvlemap  15391  dvidlemap  15402  dvidrelem  15403  dvidsslem  15404  dvcnp2cntop  15410  dvaddxxbr  15412  dvmulxxbr  15413  dvcoapbr  15418  dvcjbr  15419  dvrecap  15424  dveflem  15437  logltb  15585  2irrexpqap  15689  sgmnncl  15699  dvdsppwf1o  15700  mpodvdsmulf1o  15701  perfectlem2  15711  lgsmod  15742  lgsne0  15754  gausslemma2dlem4  15780  2sqlem6  15836  2sqlem8  15839  2sqlem10  15841  upgrm  15937  upgr1or2  15938  umgredg2en  15946  umgrbien  15947  upgr1elem1  15957  edgupgren  15976  edgumgren  15977  umgredgnlp  15987  edgusgren  15998  usgruspgrben  16021  usgr1e  16076  wlkvtxiedg  16133  wlkvtxiedgg  16134  istrl  16171  pw1nct  16514  sbthom  16540  trilpo  16557  trirec0  16558  reap0  16572  cndcap  16573  dcapnconst  16575  neapmkv  16582  neap0mkv  16583  ltlenmkv  16584