Theorem breq1 4086

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

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

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breq12  4088  breq1i  4090  breq1d  4093  nbrne2  4103  brab1  4131  pocl  4394  swopolem  4396  swopo  4397  issod  4410  sowlin  4411  sotritrieq  4416  frirrg  4441  wetriext  4669  vtoclr  4767  brcog  4889  brcogw  4891  opelcnvg  4902  dfdmf  4916  eldmg  4918  dfrnf  4965  dfres2  5057  imasng  5093  coi1  5244  dffun6f  5331  funmo  5333  fun11  5388  fveq2  5629  funfveu  5642  sefvex  5650  nfunsn  5666  fvmptss2  5711  f1ompt  5788  fmptco  5803  dff13  5898  foeqcnvco  5920  isorel  5938  isocnv  5941  isotr  5946  isoini  5948  isopolem  5952  isosolem  5954  f1oiso  5956  f1oiso2  5957  caovordig  6177  caovordg  6179  caovord3d  6182  caovord  6183  caovord3  6185  caofrss  6256  caoftrn  6257  poxp  6384  brtpos2  6403  rntpos  6409  tpostpos  6416  ertr  6703  ecopovsym  6786  ecopovtrn  6787  ecopovsymg  6789  ecopovtrng  6790  th3qlem2  6793  isfi  6920  en0  6955  en1  6959  en1bg  6960  endisj  6991  xpcomco  6993  dom0  7007  ssenen  7020  nneneq  7026  domfiexmid  7048  findcard  7058  findcard2  7059  findcard2s  7060  isinfinf  7067  tridc  7070  fimax2gtrilemstep  7071  fimax2gtri  7072  fiintim  7104  fisseneq  7107  en1eqsnbi  7127  isbth  7145  supmoti  7171  eqsupti  7174  supubti  7177  suplubti  7178  supsnti  7183  isotilem  7184  isoti  7185  supisolem  7186  supisoex  7187  infminti  7205  isnumi  7365  cardval3ex  7368  oncardval  7369  cardonle  7370  en2prde  7377  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidapne  7457  nqtri3or  7594  ltsonq  7596  ltanqg  7598  ltmnqg  7599  ltexnqq  7606  subhalfnqq  7612  ltbtwnnqq  7613  archnqq  7615  nqnq0pi  7636  prcdnql  7682  prcunqu  7683  prnmaxl  7686  genpcuu  7718  genprndl  7719  genprndu  7720  nqprm  7740  nqprrnd  7741  nqprdisj  7742  nqprloc  7743  nqpru  7750  addnqprlemrl  7755  addnqprlemfl  7757  addnqprlemfu  7758  prmuloc2  7765  mulnqprlemrl  7771  mulnqprlemfl  7773  mulnqprlemfu  7774  1idprl  7788  ltnqpr  7791  ltnqpri  7792  prplnqu  7818  recexprlemell  7820  recexprlemm  7822  recexprlemdisj  7828  recexprlemloc  7829  recexprlem1ssu  7832  recexprlemss1l  7833  aptiprlemu  7838  archpr  7841  cauappcvgprlemm  7843  cauappcvgprlemladdfl  7853  cauappcvgprlem2  7858  cauappcvgpr  7860  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemcl  7874  caucvgprlem2  7878  caucvgpr  7880  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnbj  7891  caucvgprprlemmu  7893  caucvgprprlemopu  7897  caucvgprprlemexbt  7904  caucvgprprlemaddq  7906  caucvgprprlem1  7907  caucvgprprlem2  7908  caucvgprpr  7910  suplocexprlemmu  7916  suplocexprlemloc  7919  suplocexpr  7923  lttrsr  7960  ltsosr  7962  1ne0sr  7964  ltasrg  7968  aptisr  7977  mulextsr1  7979  archsr  7980  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  caucvgsr  8000  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axpre-ltwlin  8081  axpre-lttrn  8082  axpre-apti  8083  axpre-ltadd  8084  axpre-mulext  8086  axcaucvglemcau  8096  axcaucvglemres  8097  axcaucvg  8098  axpre-suploclemres  8099  axpre-suploc  8100  ltxrlt  8223  lttri3  8237  ltordlem  8640  lt0ne0d  8671  reapti  8737  apreim  8761  apsscn  8805  recexap  8811  lbreu  9103  lble  9105  suprleubex  9112  sup3exmid  9115  nnsub  9160  nominpos  9360  nn0n0n1ge2b  9537  zextle  9549  fzind  9573  btwnz  9577  uzval  9735  supinfneg  9802  infsupneg  9803  infregelbex  9805  ublbneg  9820  lbzbi  9823  qreccl  9849  xrltnsym  10001  xrlttr  10003  xrltso  10004  xrlttri3  10005  nltpnft  10022  npnflt  10023  xrrebnd  10027  xltnegi  10043  xnn0lenn0nn0  10073  xsubge0  10089  xlesubadd  10091  xleaddadd  10095  ixxval  10104  elixx1  10105  elioo2  10129  iccid  10133  fzval  10218  elfz1  10221  zsupcllemstep  10461  suprzubdc  10468  zsupssdc  10470  qtri3or  10472  exbtwnzlemstep  10479  exbtwnzlemshrink  10480  exbtwnzlemex  10481  exbtwnz  10482  rebtwn2zlemstep  10484  rebtwn2zlemshrink  10485  rebtwn2z  10486  qbtwnre  10488  qbtwnxr  10489  flval  10504  flqlelt  10508  flqbi  10522  flqeqceilz  10552  modqid2  10585  seq3f1olemqsum  10747  seq3f1oleml  10750  seq3f1o  10751  seqf1oglem2  10754  expcl2lemap  10785  expclzaplem  10797  expclzap  10798  expap0i  10805  nn0ltexp2  10943  hashinfuni  11011  hashennnuni  11013  hashunlem  11038  zfz1isolemiso  11074  zfz1isolem1  11075  zfz1iso  11076  absle  11616  maxleast  11740  rexanre  11747  rexico  11748  fimaxre2  11754  minmax  11757  xrmaxltsup  11785  xrminmax  11792  climshft  11831  reccn2ap  11840  summodclem3  11907  summodclem2a  11908  summodc  11910  zsumdc  11911  fsum3  11914  fsum3cvg3  11923  fsumcl2lem  11925  fsumadd  11933  sumsnf  11936  fsummulc2  11975  isumlessdc  12023  cvgratz  12059  mertenslemi1  12062  ntrivcvgap0  12076  prodmodclem3  12102  prodmodclem2a  12103  prodmodc  12105  zproddc  12106  fprodseq  12110  fprodntrivap  12111  fprodmul  12118  prodsnf  12119  absdvdsb  12336  zdvdsdc  12339  dvdsabseq  12374  dvdsdivcl  12377  dvdsext  12382  divalglemnn  12445  divalglemeunn  12448  divalglemeuneg  12450  divalgmod  12454  ndvdssub  12457  gcdsupex  12494  gcdsupcl  12495  gcddvds  12500  dvdslegcd  12501  bezoutlemmain  12535  bezoutlemex  12538  bezoutlemzz  12539  bezoutlemmo  12543  bezoutlemeu  12544  bezoutlemle  12545  bezoutlemsup  12546  dfgcd3  12547  dfgcd2  12551  gcdzeq  12559  dvdssq  12568  nnwodc  12573  uzwodc  12574  nnwofdc  12575  nn0seqcvgd  12579  algcvgblem  12587  lcmval  12601  lcmdvds  12617  lcmgcdeq  12621  coprmgcdb  12626  ncoprmgcdne1b  12627  coprmdvds1  12629  1nprm  12652  1idssfct  12653  isprm2lem  12654  isprm2  12655  dvdsprime  12660  nprm  12661  3prm  12666  dvdsprm  12675  exprmfct  12676  isprm5lem  12679  isprm5  12680  coprm  12682  sqrt2irr  12700  dvdsfi  12777  phisum  12779  odzval  12780  pythagtriplem4  12807  pc2dvds  12869  pcprmpw2  12872  pcprmpw  12873  dvdsprmpweqle  12876  oddprmdvds  12893  prmpwdvds  12894  pockthg  12896  1arith  12906  exmidunben  13013  nninfdclemcl  13035  nninfdclemp1  13037  nninfdc  13040  imasaddfnlemg  13363  cnfldui  14569  znleval  14633  ssblex  15121  comet  15189  bdmopn  15194  reopnap  15236  divcnap  15255  cdivcncfap  15294  cnopnap  15301  divcncfap  15304  maxcncf  15305  mincncf  15306  dedekindeulemuub  15307  dedekindeulemloc  15309  dedekindeulemlu  15311  dedekindeulemeu  15312  dedekindeu  15313  suplociccreex  15314  dedekindicclemuub  15316  dedekindicclemloc  15318  dedekindicclemlu  15320  dedekindicclemeu  15321  dedekindicclemicc  15322  dedekindicc  15323  ivthinclemlopn  15326  ivthinclemlr  15327  ivthinclemuopn  15328  ivthinclemur  15329  ivthinclemloc  15331  ivthinc  15333  ivthreinc  15335  dich0  15342  ivthdich  15343  limcdifap  15352  limcimolemlt  15354  limccoap  15368  dvlemap  15370  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvcnp2cntop  15389  dvaddxxbr  15391  dvmulxxbr  15392  dvcoapbr  15397  dvcjbr  15398  dvrecap  15403  dveflem  15416  logltb  15564  2irrexpqap  15668  sgmnncl  15678  dvdsppwf1o  15679  mpodvdsmulf1o  15680  perfectlem2  15690  lgsmod  15721  lgsne0  15733  gausslemma2dlem4  15759  2sqlem6  15815  2sqlem8  15818  2sqlem10  15820  upgrm  15916  upgr1or2  15917  umgredg2en  15925  umgrbien  15926  upgr1elem1  15936  edgupgren  15955  edgumgren  15956  umgredgnlp  15966  edgusgren  15977  usgruspgrben  16000  wlkvtxiedg  16091  wlkvtxiedgg  16092  istrl  16129  pw1nct  16456  sbthom  16482  trilpo  16499  trirec0  16500  reap0  16514  cndcap  16515  dcapnconst  16517  neapmkv  16524  neap0mkv  16525  ltlenmkv  16526