Theorem breq1 3984

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1343   ∈ wcel 2136  ⟨cop 3578   class class class wbr 3981

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-br 3982

This theorem is referenced by:  breq12  3986  breq1i  3988  breq1d  3991  nbrne2  4001  brab1  4028  pocl  4280  swopolem  4282  swopo  4283  issod  4296  sowlin  4297  sotritrieq  4302  frirrg  4327  wetriext  4553  vtoclr  4651  brcog  4770  brcogw  4772  opelcnvg  4783  dfdmf  4796  eldmg  4798  dfrnf  4844  dfres2  4935  imasng  4968  coi1  5118  dffun6f  5200  funmo  5202  fun11  5254  fveq2  5485  funfveu  5498  sefvex  5506  nfunsn  5519  fvmptss2  5560  f1ompt  5635  fmptco  5650  dff13  5735  foeqcnvco  5757  isorel  5775  isocnv  5778  isotr  5783  isoini  5785  isopolem  5789  isosolem  5791  f1oiso  5793  f1oiso2  5794  caovordig  6003  caovordg  6005  caovord3d  6008  caovord  6009  caovord3  6011  caofrss  6073  caoftrn  6074  poxp  6196  brtpos2  6215  rntpos  6221  tpostpos  6228  ertr  6512  ecopovsym  6593  ecopovtrn  6594  ecopovsymg  6596  ecopovtrng  6597  th3qlem2  6600  isfi  6723  en0  6757  en1  6761  en1bg  6762  endisj  6786  xpcomco  6788  dom0  6800  ssenen  6813  nneneq  6819  domfiexmid  6840  findcard  6850  findcard2  6851  findcard2s  6852  isinfinf  6859  tridc  6861  fimax2gtrilemstep  6862  fimax2gtri  6863  fiintim  6890  fisseneq  6893  en1eqsnbi  6910  isbth  6928  supmoti  6954  eqsupti  6957  supubti  6960  suplubti  6961  supsnti  6966  isotilem  6967  isoti  6968  supisolem  6969  supisoex  6970  infminti  6988  isnumi  7134  cardval3ex  7137  oncardval  7138  cardonle  7139  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  nqtri3or  7333  ltsonq  7335  ltanqg  7337  ltmnqg  7338  ltexnqq  7345  subhalfnqq  7351  ltbtwnnqq  7352  archnqq  7354  nqnq0pi  7375  prcdnql  7421  prcunqu  7422  prnmaxl  7425  genpcuu  7457  genprndl  7458  genprndu  7459  nqprm  7479  nqprrnd  7480  nqprdisj  7481  nqprloc  7482  nqpru  7489  addnqprlemrl  7494  addnqprlemfl  7496  addnqprlemfu  7497  prmuloc2  7504  mulnqprlemrl  7510  mulnqprlemfl  7512  mulnqprlemfu  7513  1idprl  7527  ltnqpr  7530  ltnqpri  7531  prplnqu  7557  recexprlemell  7559  recexprlemm  7561  recexprlemdisj  7567  recexprlemloc  7568  recexprlem1ssu  7571  recexprlemss1l  7572  aptiprlemu  7577  archpr  7580  cauappcvgprlemm  7582  cauappcvgprlemladdfl  7592  cauappcvgprlem2  7597  cauappcvgpr  7599  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemcl  7613  caucvgprlem2  7617  caucvgpr  7619  caucvgprprlemelu  7623  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemnbj  7630  caucvgprprlemmu  7632  caucvgprprlemopu  7636  caucvgprprlemexbt  7643  caucvgprprlemaddq  7645  caucvgprprlem1  7646  caucvgprprlem2  7647  caucvgprpr  7649  suplocexprlemmu  7655  suplocexprlemloc  7658  suplocexpr  7662  lttrsr  7699  ltsosr  7701  1ne0sr  7703  ltasrg  7707  aptisr  7716  mulextsr1  7718  archsr  7719  caucvgsrlemgt1  7732  caucvgsrlemoffres  7737  caucvgsr  7739  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  axpre-ltwlin  7820  axpre-lttrn  7821  axpre-apti  7822  axpre-ltadd  7823  axpre-mulext  7825  axcaucvglemcau  7835  axcaucvglemres  7836  axcaucvg  7837  axpre-suploclemres  7838  axpre-suploc  7839  ltxrlt  7960  lttri3  7974  ltordlem  8376  lt0ne0d  8407  reapti  8473  apreim  8497  apsscn  8541  recexap  8546  lbreu  8836  lble  8838  suprleubex  8845  sup3exmid  8848  nnsub  8892  nominpos  9090  nn0n0n1ge2b  9266  zextle  9278  fzind  9302  btwnz  9306  uzval  9464  supinfneg  9529  infsupneg  9530  infregelbex  9532  ublbneg  9547  lbzbi  9550  qreccl  9576  xrltnsym  9725  xrlttr  9727  xrltso  9728  xrlttri3  9729  nltpnft  9746  npnflt  9747  xrrebnd  9751  xltnegi  9767  xnn0lenn0nn0  9797  xsubge0  9813  xlesubadd  9815  xleaddadd  9819  ixxval  9828  elixx1  9829  elioo2  9853  iccid  9857  fzval  9942  elfz1  9945  qtri3or  10174  exbtwnzlemstep  10179  exbtwnzlemshrink  10180  exbtwnzlemex  10181  exbtwnz  10182  rebtwn2zlemstep  10184  rebtwn2zlemshrink  10185  rebtwn2z  10186  qbtwnre  10188  qbtwnxr  10189  flval  10203  flqlelt  10207  flqbi  10221  flqeqceilz  10249  modqid2  10282  seq3f1olemqsum  10431  seq3f1oleml  10434  seq3f1o  10435  expcl2lemap  10463  expclzaplem  10475  expclzap  10476  expap0i  10483  nn0ltexp2  10619  hashinfuni  10686  hashennnuni  10688  hashunlem  10713  zfz1isolemiso  10748  zfz1isolem1  10749  zfz1iso  10750  absle  11027  maxleast  11151  rexanre  11158  rexico  11159  fimaxre2  11164  minmax  11167  xrmaxltsup  11195  xrminmax  11202  climshft  11241  reccn2ap  11250  summodclem3  11317  summodclem2a  11318  summodc  11320  zsumdc  11321  fsum3  11324  fsum3cvg3  11333  fsumcl2lem  11335  fsumadd  11343  sumsnf  11346  fsummulc2  11385  isumlessdc  11433  cvgratz  11469  mertenslemi1  11472  ntrivcvgap0  11486  prodmodclem3  11512  prodmodclem2a  11513  prodmodc  11515  zproddc  11516  fprodseq  11520  fprodntrivap  11521  fprodmul  11528  prodsnf  11529  absdvdsb  11745  zdvdsdc  11748  dvdsabseq  11781  dvdsdivcl  11784  dvdsext  11789  divalglemnn  11851  divalglemeunn  11854  divalglemeuneg  11856  divalgmod  11860  ndvdssub  11863  zsupcllemstep  11874  suprzubdc  11881  zsupssdc  11883  gcdsupex  11886  gcdsupcl  11887  gcddvds  11892  dvdslegcd  11893  bezoutlemmain  11927  bezoutlemex  11930  bezoutlemzz  11931  bezoutlemmo  11935  bezoutlemeu  11936  bezoutlemle  11937  bezoutlemsup  11938  dfgcd3  11939  dfgcd2  11943  gcdzeq  11951  dvdssq  11960  nnwodc  11965  uzwodc  11966  nnwofdc  11967  nn0seqcvgd  11969  algcvgblem  11977  lcmval  11991  lcmdvds  12007  lcmgcdeq  12011  coprmgcdb  12016  ncoprmgcdne1b  12017  coprmdvds1  12019  1nprm  12042  1idssfct  12043  isprm2lem  12044  isprm2  12045  dvdsprime  12050  nprm  12051  3prm  12056  dvdsprm  12065  exprmfct  12066  isprm5lem  12069  isprm5  12070  coprm  12072  sqrt2irr  12090  phisum  12168  odzval  12169  pythagtriplem4  12196  pc2dvds  12257  pcprmpw2  12260  pcprmpw  12261  dvdsprmpweqle  12264  oddprmdvds  12280  prmpwdvds  12281  pockthg  12283  1arith  12293  exmidunben  12355  nninfdclemcl  12377  nninfdclemp1  12379  nninfdc  12382  ssblex  13031  comet  13099  bdmopn  13104  reopnap  13138  divcnap  13155  cdivcncfap  13187  cnopnap  13194  dedekindeulemuub  13195  dedekindeulemloc  13197  dedekindeulemlu  13199  dedekindeulemeu  13200  dedekindeu  13201  suplociccreex  13202  dedekindicclemuub  13204  dedekindicclemloc  13206  dedekindicclemlu  13208  dedekindicclemeu  13209  dedekindicclemicc  13210  dedekindicc  13211  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemloc  13219  ivthinc  13221  limcdifap  13231  limcimolemlt  13233  limccoap  13247  dvlemap  13249  dvidlemap  13260  dvcnp2cntop  13263  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvcjbr  13272  dvrecap  13277  dveflem  13287  logltb  13395  2irrexpqap  13496  lgsmod  13527  lgsne0  13539  2sqlem6  13556  2sqlem8  13559  2sqlem10  13561  pw1nct  13843  sbthom  13865  trilpo  13882  trirec0  13883  reap0  13897  dcapnconst  13899  neapmkv  13906