Theorem breq1 4006

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2148  ⟨cop 3595   class class class wbr 4003

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004

This theorem is referenced by:  breq12  4008  breq1i  4010  breq1d  4013  nbrne2  4023  brab1  4050  pocl  4303  swopolem  4305  swopo  4306  issod  4319  sowlin  4320  sotritrieq  4325  frirrg  4350  wetriext  4576  vtoclr  4674  brcog  4794  brcogw  4796  opelcnvg  4807  dfdmf  4820  eldmg  4822  dfrnf  4868  dfres2  4959  imasng  4993  coi1  5144  dffun6f  5229  funmo  5231  fun11  5283  fveq2  5515  funfveu  5528  sefvex  5536  nfunsn  5549  fvmptss2  5591  f1ompt  5667  fmptco  5682  dff13  5768  foeqcnvco  5790  isorel  5808  isocnv  5811  isotr  5816  isoini  5818  isopolem  5822  isosolem  5824  f1oiso  5826  f1oiso2  5827  caovordig  6039  caovordg  6041  caovord3d  6044  caovord  6045  caovord3  6047  caofrss  6106  caoftrn  6107  poxp  6232  brtpos2  6251  rntpos  6257  tpostpos  6264  ertr  6549  ecopovsym  6630  ecopovtrn  6631  ecopovsymg  6633  ecopovtrng  6634  th3qlem2  6637  isfi  6760  en0  6794  en1  6798  en1bg  6799  endisj  6823  xpcomco  6825  dom0  6837  ssenen  6850  nneneq  6856  domfiexmid  6877  findcard  6887  findcard2  6888  findcard2s  6889  isinfinf  6896  tridc  6898  fimax2gtrilemstep  6899  fimax2gtri  6900  fiintim  6927  fisseneq  6930  en1eqsnbi  6947  isbth  6965  supmoti  6991  eqsupti  6994  supubti  6997  suplubti  6998  supsnti  7003  isotilem  7004  isoti  7005  supisolem  7006  supisoex  7007  infminti  7025  isnumi  7180  cardval3ex  7183  oncardval  7184  cardonle  7185  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidapne  7258  nqtri3or  7394  ltsonq  7396  ltanqg  7398  ltmnqg  7399  ltexnqq  7406  subhalfnqq  7412  ltbtwnnqq  7413  archnqq  7415  nqnq0pi  7436  prcdnql  7482  prcunqu  7483  prnmaxl  7486  genpcuu  7518  genprndl  7519  genprndu  7520  nqprm  7540  nqprrnd  7541  nqprdisj  7542  nqprloc  7543  nqpru  7550  addnqprlemrl  7555  addnqprlemfl  7557  addnqprlemfu  7558  prmuloc2  7565  mulnqprlemrl  7571  mulnqprlemfl  7573  mulnqprlemfu  7574  1idprl  7588  ltnqpr  7591  ltnqpri  7592  prplnqu  7618  recexprlemell  7620  recexprlemm  7622  recexprlemdisj  7628  recexprlemloc  7629  recexprlem1ssu  7632  recexprlemss1l  7633  aptiprlemu  7638  archpr  7641  cauappcvgprlemm  7643  cauappcvgprlemladdfl  7653  cauappcvgprlem2  7658  cauappcvgpr  7660  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemcl  7674  caucvgprlem2  7678  caucvgpr  7680  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnbj  7691  caucvgprprlemmu  7693  caucvgprprlemopu  7697  caucvgprprlemexbt  7704  caucvgprprlemaddq  7706  caucvgprprlem1  7707  caucvgprprlem2  7708  caucvgprpr  7710  suplocexprlemmu  7716  suplocexprlemloc  7719  suplocexpr  7723  lttrsr  7760  ltsosr  7762  1ne0sr  7764  ltasrg  7768  aptisr  7777  mulextsr1  7779  archsr  7780  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  caucvgsr  7800  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  axpre-ltwlin  7881  axpre-lttrn  7882  axpre-apti  7883  axpre-ltadd  7884  axpre-mulext  7886  axcaucvglemcau  7896  axcaucvglemres  7897  axcaucvg  7898  axpre-suploclemres  7899  axpre-suploc  7900  ltxrlt  8021  lttri3  8035  ltordlem  8437  lt0ne0d  8468  reapti  8534  apreim  8558  apsscn  8602  recexap  8608  lbreu  8900  lble  8902  suprleubex  8909  sup3exmid  8912  nnsub  8956  nominpos  9154  nn0n0n1ge2b  9330  zextle  9342  fzind  9366  btwnz  9370  uzval  9528  supinfneg  9593  infsupneg  9594  infregelbex  9596  ublbneg  9611  lbzbi  9614  qreccl  9640  xrltnsym  9791  xrlttr  9793  xrltso  9794  xrlttri3  9795  nltpnft  9812  npnflt  9813  xrrebnd  9817  xltnegi  9833  xnn0lenn0nn0  9863  xsubge0  9879  xlesubadd  9881  xleaddadd  9885  ixxval  9894  elixx1  9895  elioo2  9919  iccid  9923  fzval  10008  elfz1  10011  qtri3or  10240  exbtwnzlemstep  10245  exbtwnzlemshrink  10246  exbtwnzlemex  10247  exbtwnz  10248  rebtwn2zlemstep  10250  rebtwn2zlemshrink  10251  rebtwn2z  10252  qbtwnre  10254  qbtwnxr  10255  flval  10269  flqlelt  10273  flqbi  10287  flqeqceilz  10315  modqid2  10348  seq3f1olemqsum  10497  seq3f1oleml  10500  seq3f1o  10501  expcl2lemap  10529  expclzaplem  10541  expclzap  10542  expap0i  10549  nn0ltexp2  10685  hashinfuni  10752  hashennnuni  10754  hashunlem  10779  zfz1isolemiso  10814  zfz1isolem1  10815  zfz1iso  10816  absle  11093  maxleast  11217  rexanre  11224  rexico  11225  fimaxre2  11230  minmax  11233  xrmaxltsup  11261  xrminmax  11268  climshft  11307  reccn2ap  11316  summodclem3  11383  summodclem2a  11384  summodc  11386  zsumdc  11387  fsum3  11390  fsum3cvg3  11399  fsumcl2lem  11401  fsumadd  11409  sumsnf  11412  fsummulc2  11451  isumlessdc  11499  cvgratz  11535  mertenslemi1  11538  ntrivcvgap0  11552  prodmodclem3  11578  prodmodclem2a  11579  prodmodc  11581  zproddc  11582  fprodseq  11586  fprodntrivap  11587  fprodmul  11594  prodsnf  11595  absdvdsb  11811  zdvdsdc  11814  dvdsabseq  11847  dvdsdivcl  11850  dvdsext  11855  divalglemnn  11917  divalglemeunn  11920  divalglemeuneg  11922  divalgmod  11926  ndvdssub  11929  zsupcllemstep  11940  suprzubdc  11947  zsupssdc  11949  gcdsupex  11952  gcdsupcl  11953  gcddvds  11958  dvdslegcd  11959  bezoutlemmain  11993  bezoutlemex  11996  bezoutlemzz  11997  bezoutlemmo  12001  bezoutlemeu  12002  bezoutlemle  12003  bezoutlemsup  12004  dfgcd3  12005  dfgcd2  12009  gcdzeq  12017  dvdssq  12026  nnwodc  12031  uzwodc  12032  nnwofdc  12033  nn0seqcvgd  12035  algcvgblem  12043  lcmval  12057  lcmdvds  12073  lcmgcdeq  12077  coprmgcdb  12082  ncoprmgcdne1b  12083  coprmdvds1  12085  1nprm  12108  1idssfct  12109  isprm2lem  12110  isprm2  12111  dvdsprime  12116  nprm  12117  3prm  12122  dvdsprm  12131  exprmfct  12132  isprm5lem  12135  isprm5  12136  coprm  12138  sqrt2irr  12156  phisum  12234  odzval  12235  pythagtriplem4  12262  pc2dvds  12323  pcprmpw2  12326  pcprmpw  12327  dvdsprmpweqle  12330  oddprmdvds  12346  prmpwdvds  12347  pockthg  12349  1arith  12359  exmidunben  12421  nninfdclemcl  12443  nninfdclemp1  12445  nninfdc  12448  imasaddfnlemg  12717  ssblex  13824  comet  13892  bdmopn  13897  reopnap  13931  divcnap  13948  cdivcncfap  13980  cnopnap  13987  dedekindeulemuub  13988  dedekindeulemloc  13990  dedekindeulemlu  13992  dedekindeulemeu  13993  dedekindeu  13994  suplociccreex  13995  dedekindicclemuub  13997  dedekindicclemloc  13999  dedekindicclemlu  14001  dedekindicclemeu  14002  dedekindicclemicc  14003  dedekindicc  14004  ivthinclemlopn  14007  ivthinclemlr  14008  ivthinclemuopn  14009  ivthinclemur  14010  ivthinclemloc  14012  ivthinc  14014  limcdifap  14024  limcimolemlt  14026  limccoap  14040  dvlemap  14042  dvidlemap  14053  dvcnp2cntop  14056  dvaddxxbr  14058  dvmulxxbr  14059  dvcoapbr  14064  dvcjbr  14065  dvrecap  14070  dveflem  14080  logltb  14188  2irrexpqap  14289  lgsmod  14320  lgsne0  14332  2sqlem6  14349  2sqlem8  14352  2sqlem10  14354  pw1nct  14634  sbthom  14656  trilpo  14673  trirec0  14674  reap0  14688  dcapnconst  14690  neapmkv  14697  neap0mkv  14698  ltlenmkv  14699