Theorem breq1 3968

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1335   ∈ wcel 2128  ⟨cop 3563   class class class wbr 3965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-sn 3566  df-pr 3567  df-op 3569  df-br 3966

This theorem is referenced by:  breq12  3970  breq1i  3972  breq1d  3975  nbrne2  3984  brab1  4011  pocl  4263  swopolem  4265  swopo  4266  issod  4279  sowlin  4280  sotritrieq  4285  frirrg  4310  wetriext  4535  vtoclr  4633  brcog  4752  brcogw  4754  opelcnvg  4765  dfdmf  4778  eldmg  4780  dfrnf  4826  dfres2  4917  imasng  4950  coi1  5100  dffun6f  5182  funmo  5184  fun11  5236  fveq2  5467  funfveu  5480  sefvex  5488  nfunsn  5501  fvmptss2  5542  f1ompt  5617  fmptco  5632  dff13  5715  foeqcnvco  5737  isorel  5755  isocnv  5758  isotr  5763  isoini  5765  isopolem  5769  isosolem  5771  f1oiso  5773  f1oiso2  5774  caovordig  5983  caovordg  5985  caovord3d  5988  caovord  5989  caovord3  5991  caofrss  6053  caoftrn  6054  poxp  6176  brtpos2  6195  rntpos  6201  tpostpos  6208  ertr  6492  ecopovsym  6573  ecopovtrn  6574  ecopovsymg  6576  ecopovtrng  6577  th3qlem2  6580  isfi  6703  en0  6737  en1  6741  en1bg  6742  endisj  6766  xpcomco  6768  dom0  6780  ssenen  6793  nneneq  6799  domfiexmid  6820  findcard  6830  findcard2  6831  findcard2s  6832  isinfinf  6839  tridc  6841  fimax2gtrilemstep  6842  fimax2gtri  6843  fiintim  6870  fisseneq  6873  en1eqsnbi  6890  isbth  6908  supmoti  6933  eqsupti  6936  supubti  6939  suplubti  6940  supsnti  6945  isotilem  6946  isoti  6947  supisolem  6948  supisoex  6949  infminti  6967  isnumi  7111  cardval3ex  7114  oncardval  7115  cardonle  7116  exmidfodomrlemr  7131  exmidfodomrlemrALT  7132  nqtri3or  7310  ltsonq  7312  ltanqg  7314  ltmnqg  7315  ltexnqq  7322  subhalfnqq  7328  ltbtwnnqq  7329  archnqq  7331  nqnq0pi  7352  prcdnql  7398  prcunqu  7399  prnmaxl  7402  genpcuu  7434  genprndl  7435  genprndu  7436  nqprm  7456  nqprrnd  7457  nqprdisj  7458  nqprloc  7459  nqpru  7466  addnqprlemrl  7471  addnqprlemfl  7473  addnqprlemfu  7474  prmuloc2  7481  mulnqprlemrl  7487  mulnqprlemfl  7489  mulnqprlemfu  7490  1idprl  7504  ltnqpr  7507  ltnqpri  7508  prplnqu  7534  recexprlemell  7536  recexprlemm  7538  recexprlemdisj  7544  recexprlemloc  7545  recexprlem1ssu  7548  recexprlemss1l  7549  aptiprlemu  7554  archpr  7557  cauappcvgprlemm  7559  cauappcvgprlemladdfl  7569  cauappcvgprlem2  7574  cauappcvgpr  7576  caucvgprlemnkj  7580  caucvgprlemnbj  7581  caucvgprlemcl  7590  caucvgprlem2  7594  caucvgpr  7596  caucvgprprlemelu  7600  caucvgprprlemcbv  7601  caucvgprprlemval  7602  caucvgprprlemnbj  7607  caucvgprprlemmu  7609  caucvgprprlemopu  7613  caucvgprprlemexbt  7620  caucvgprprlemaddq  7622  caucvgprprlem1  7623  caucvgprprlem2  7624  caucvgprpr  7626  suplocexprlemmu  7632  suplocexprlemloc  7635  suplocexpr  7639  lttrsr  7676  ltsosr  7678  1ne0sr  7680  ltasrg  7684  aptisr  7693  mulextsr1  7695  archsr  7696  caucvgsrlemgt1  7709  caucvgsrlemoffres  7714  caucvgsr  7716  suplocsrlemb  7720  suplocsrlempr  7721  suplocsrlem  7722  axpre-ltwlin  7797  axpre-lttrn  7798  axpre-apti  7799  axpre-ltadd  7800  axpre-mulext  7802  axcaucvglemcau  7812  axcaucvglemres  7813  axcaucvg  7814  axpre-suploclemres  7815  axpre-suploc  7816  ltxrlt  7937  lttri3  7951  ltordlem  8351  lt0ne0d  8382  reapti  8448  apreim  8472  apsscn  8516  recexap  8521  lbreu  8810  lble  8812  suprleubex  8819  sup3exmid  8822  nnsub  8866  nominpos  9064  nn0n0n1ge2b  9237  zextle  9249  fzind  9273  btwnz  9277  uzval  9435  supinfneg  9500  infsupneg  9501  ublbneg  9515  lbzbi  9518  qreccl  9544  xrltnsym  9693  xrlttr  9695  xrltso  9696  xrlttri3  9697  nltpnft  9711  npnflt  9712  xrrebnd  9716  xltnegi  9732  xnn0lenn0nn0  9762  xsubge0  9778  xlesubadd  9780  xleaddadd  9784  ixxval  9793  elixx1  9794  elioo2  9818  iccid  9822  fzval  9907  elfz1  9910  qtri3or  10135  exbtwnzlemstep  10140  exbtwnzlemshrink  10141  exbtwnzlemex  10142  exbtwnz  10143  rebtwn2zlemstep  10145  rebtwn2zlemshrink  10146  rebtwn2z  10147  qbtwnre  10149  qbtwnxr  10150  flval  10164  flqlelt  10168  flqbi  10182  flqeqceilz  10210  modqid2  10243  seq3f1olemqsum  10392  seq3f1oleml  10395  seq3f1o  10396  expcl2lemap  10424  expclzaplem  10436  expclzap  10437  expap0i  10444  hashinfuni  10644  hashennnuni  10646  hashunlem  10671  zfz1isolemiso  10703  zfz1isolem1  10704  zfz1iso  10705  absle  10982  maxleast  11106  rexanre  11113  rexico  11114  fimaxre2  11119  minmax  11122  xrmaxltsup  11148  xrminmax  11155  climshft  11194  reccn2ap  11203  summodclem3  11270  summodclem2a  11271  summodc  11273  zsumdc  11274  fsum3  11277  fsum3cvg3  11286  fsumcl2lem  11288  fsumadd  11296  sumsnf  11299  fsummulc2  11338  isumlessdc  11386  cvgratz  11422  mertenslemi1  11425  ntrivcvgap0  11439  prodmodclem3  11465  prodmodclem2a  11466  prodmodc  11468  zproddc  11469  fprodseq  11473  fprodntrivap  11474  fprodmul  11481  prodsnf  11482  absdvdsb  11697  zdvdsdc  11700  dvdsabseq  11731  dvdsdivcl  11734  dvdsext  11739  divalglemnn  11801  divalglemeunn  11804  divalglemeuneg  11806  divalgmod  11810  ndvdssub  11813  zsupcllemstep  11824  gcdsupex  11832  gcdsupcl  11833  gcddvds  11838  dvdslegcd  11839  bezoutlemmain  11873  bezoutlemex  11876  bezoutlemzz  11877  bezoutlemmo  11881  bezoutlemeu  11882  bezoutlemle  11883  bezoutlemsup  11884  dfgcd3  11885  dfgcd2  11889  gcdzeq  11897  dvdssq  11906  nn0seqcvgd  11909  algcvgblem  11917  lcmval  11931  lcmdvds  11947  lcmgcdeq  11951  coprmgcdb  11956  ncoprmgcdne1b  11957  coprmdvds1  11959  1nprm  11982  1idssfct  11983  isprm2lem  11984  isprm2  11985  dvdsprime  11990  nprm  11991  3prm  11996  dvdsprm  12004  exprmfct  12005  coprm  12009  sqrt2irr  12027  phisum  12103  exmidunben  12138  ssblex  12802  comet  12870  bdmopn  12875  reopnap  12909  divcnap  12926  cdivcncfap  12958  cnopnap  12965  dedekindeulemuub  12966  dedekindeulemloc  12968  dedekindeulemlu  12970  dedekindeulemeu  12971  dedekindeu  12972  suplociccreex  12973  dedekindicclemuub  12975  dedekindicclemloc  12977  dedekindicclemlu  12979  dedekindicclemeu  12980  dedekindicclemicc  12981  dedekindicc  12982  ivthinclemlopn  12985  ivthinclemlr  12986  ivthinclemuopn  12987  ivthinclemur  12988  ivthinclemloc  12990  ivthinc  12992  limcdifap  13002  limcimolemlt  13004  limccoap  13018  dvlemap  13020  dvidlemap  13031  dvcnp2cntop  13034  dvaddxxbr  13036  dvmulxxbr  13037  dvcoapbr  13042  dvcjbr  13043  dvrecap  13048  dveflem  13058  logltb  13166  2irrexpqap  13266  pw1nct  13546  sbthom  13568  trilpo  13585  trirec0  13586  reap0  13600  dcapnconst  13602  neapmkv  13609