Theorem breq1 4096

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2202  ⟨cop 3676   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  breq12  4098  breq1i  4100  breq1d  4103  nbrne2  4113  brab1  4141  pocl  4406  swopolem  4408  swopo  4409  issod  4422  sowlin  4423  sotritrieq  4428  frirrg  4453  wetriext  4681  vtoclr  4780  brcog  4903  brcogw  4905  opelcnvg  4916  dfdmf  4930  eldmg  4932  dfrnf  4979  dfres2  5071  imasng  5108  coi1  5259  dffun6f  5346  funmo  5348  fun11  5404  fveq2  5648  funfveu  5661  sefvex  5669  nfunsn  5685  fvmptss2  5730  f1ompt  5806  fmptco  5821  dff13  5919  foeqcnvco  5941  isorel  5959  isocnv  5962  isotr  5967  isoini  5969  isopolem  5973  isosolem  5975  f1oiso  5977  f1oiso2  5978  caovordig  6198  caovordg  6200  caovord3d  6203  caovord  6204  caovord3  6206  caofrss  6276  caoftrn  6277  poxp  6406  brtpos2  6460  rntpos  6466  tpostpos  6473  ertr  6760  ecopovsym  6843  ecopovtrn  6844  ecopovsymg  6846  ecopovtrng  6847  th3qlem2  6850  isfi  6977  en0  7012  en1  7016  en1bg  7017  endisj  7051  xpcomco  7053  dom0  7067  ssenen  7080  nneneq  7086  domfiexmid  7110  findcard  7120  findcard2  7121  findcard2s  7122  isinfinf  7129  tridc  7132  fimax2gtrilemstep  7133  fimax2gtri  7134  fiintim  7166  fisseneq  7170  en1eqsnbi  7191  isbth  7209  supmoti  7252  eqsupti  7255  supubti  7258  suplubti  7259  supsnti  7264  isotilem  7265  isoti  7266  supisolem  7267  supisoex  7268  infminti  7286  isnumi  7446  cardval3ex  7449  oncardval  7450  cardonle  7451  en2prde  7458  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  exmidapne  7539  nqtri3or  7676  ltsonq  7678  ltanqg  7680  ltmnqg  7681  ltexnqq  7688  subhalfnqq  7694  ltbtwnnqq  7695  archnqq  7697  nqnq0pi  7718  prcdnql  7764  prcunqu  7765  prnmaxl  7768  genpcuu  7800  genprndl  7801  genprndu  7802  nqprm  7822  nqprrnd  7823  nqprdisj  7824  nqprloc  7825  nqpru  7832  addnqprlemrl  7837  addnqprlemfl  7839  addnqprlemfu  7840  prmuloc2  7847  mulnqprlemrl  7853  mulnqprlemfl  7855  mulnqprlemfu  7856  1idprl  7870  ltnqpr  7873  ltnqpri  7874  prplnqu  7900  recexprlemell  7902  recexprlemm  7904  recexprlemdisj  7910  recexprlemloc  7911  recexprlem1ssu  7914  recexprlemss1l  7915  aptiprlemu  7920  archpr  7923  cauappcvgprlemm  7925  cauappcvgprlemladdfl  7935  cauappcvgprlem2  7940  cauappcvgpr  7942  caucvgprlemnkj  7946  caucvgprlemnbj  7947  caucvgprlemcl  7956  caucvgprlem2  7960  caucvgpr  7962  caucvgprprlemelu  7966  caucvgprprlemcbv  7967  caucvgprprlemval  7968  caucvgprprlemnbj  7973  caucvgprprlemmu  7975  caucvgprprlemopu  7979  caucvgprprlemexbt  7986  caucvgprprlemaddq  7988  caucvgprprlem1  7989  caucvgprprlem2  7990  caucvgprpr  7992  suplocexprlemmu  7998  suplocexprlemloc  8001  suplocexpr  8005  lttrsr  8042  ltsosr  8044  1ne0sr  8046  ltasrg  8050  aptisr  8059  mulextsr1  8061  archsr  8062  caucvgsrlemgt1  8075  caucvgsrlemoffres  8080  caucvgsr  8082  suplocsrlemb  8086  suplocsrlempr  8087  suplocsrlem  8088  axpre-ltwlin  8163  axpre-lttrn  8164  axpre-apti  8165  axpre-ltadd  8166  axpre-mulext  8168  axcaucvglemcau  8178  axcaucvglemres  8179  axcaucvg  8180  axpre-suploclemres  8181  axpre-suploc  8182  ltxrlt  8304  lttri3  8318  ltordlem  8721  lt0ne0d  8752  reapti  8818  apreim  8842  apsscn  8886  recexap  8892  lbreu  9184  lble  9186  suprleubex  9193  sup3exmid  9196  nnsub  9241  nominpos  9441  nn0n0n1ge2b  9620  zextle  9632  fzind  9656  btwnz  9660  uzval  9818  supinfneg  9890  infsupneg  9891  infregelbex  9893  ublbneg  9908  lbzbi  9911  qreccl  9937  xrltnsym  10089  xrlttr  10091  xrltso  10092  xrlttri3  10093  nltpnft  10110  npnflt  10111  xrrebnd  10115  xltnegi  10131  xnn0lenn0nn0  10161  xsubge0  10177  xlesubadd  10179  xleaddadd  10183  ixxval  10192  elixx1  10193  elioo2  10217  iccid  10221  fzval  10307  elfz1  10310  zsupcllemstep  10552  suprzubdc  10559  zsupssdc  10561  qtri3or  10563  exbtwnzlemstep  10570  exbtwnzlemshrink  10571  exbtwnzlemex  10572  exbtwnz  10573  rebtwn2zlemstep  10575  rebtwn2zlemshrink  10576  rebtwn2z  10577  qbtwnre  10579  qbtwnxr  10580  flval  10595  flqlelt  10599  flqbi  10613  flqeqceilz  10643  modqid2  10676  seq3f1olemqsum  10838  seq3f1oleml  10841  seq3f1o  10842  seqf1oglem2  10845  expcl2lemap  10876  expclzaplem  10888  expclzap  10889  expap0i  10896  nn0ltexp2  11034  hashinfuni  11102  hashennnuni  11104  hashunlem  11130  zfz1isolemiso  11166  zfz1isolem1  11167  zfz1iso  11168  absle  11729  maxleast  11853  rexanre  11860  rexico  11861  fimaxre2  11867  minmax  11870  xrmaxltsup  11898  xrminmax  11905  climshft  11944  reccn2ap  11953  summodclem3  12021  summodclem2a  12022  summodc  12024  zsumdc  12025  fsum3  12028  fsum3cvg3  12037  fsumcl2lem  12039  fsumadd  12047  sumsnf  12050  fsummulc2  12089  isumlessdc  12137  cvgratz  12173  mertenslemi1  12176  ntrivcvgap0  12190  prodmodclem3  12216  prodmodclem2a  12217  prodmodc  12219  zproddc  12220  fprodseq  12224  fprodntrivap  12225  fprodmul  12232  prodsnf  12233  absdvdsb  12450  zdvdsdc  12453  dvdsabseq  12488  dvdsdivcl  12491  dvdsext  12496  divalglemnn  12559  divalglemeunn  12562  divalglemeuneg  12564  divalgmod  12568  ndvdssub  12571  gcdsupex  12608  gcdsupcl  12609  gcddvds  12614  dvdslegcd  12615  bezoutlemmain  12649  bezoutlemex  12652  bezoutlemzz  12653  bezoutlemmo  12657  bezoutlemeu  12658  bezoutlemle  12659  bezoutlemsup  12660  dfgcd3  12661  dfgcd2  12665  gcdzeq  12673  dvdssq  12682  nnwodc  12687  uzwodc  12688  nnwofdc  12689  nn0seqcvgd  12693  algcvgblem  12701  lcmval  12715  lcmdvds  12731  lcmgcdeq  12735  coprmgcdb  12740  ncoprmgcdne1b  12741  coprmdvds1  12743  1nprm  12766  1idssfct  12767  isprm2lem  12768  isprm2  12769  dvdsprime  12774  nprm  12775  3prm  12780  dvdsprm  12789  exprmfct  12790  isprm5lem  12793  isprm5  12794  coprm  12796  sqrt2irr  12814  dvdsfi  12891  phisum  12893  odzval  12894  pythagtriplem4  12921  pc2dvds  12983  pcprmpw2  12986  pcprmpw  12987  dvdsprmpweqle  12990  oddprmdvds  13007  prmpwdvds  13008  pockthg  13010  1arith  13020  exmidunben  13127  nninfdclemcl  13149  nninfdclemp1  13151  nninfdc  13154  imasaddfnlemg  13477  cnfldui  14685  znleval  14749  psrbagconcl  14773  ssblex  15242  comet  15310  bdmopn  15315  reopnap  15357  divcnap  15376  cdivcncfap  15415  cnopnap  15422  divcncfap  15425  maxcncf  15426  mincncf  15427  dedekindeulemuub  15428  dedekindeulemloc  15430  dedekindeulemlu  15432  dedekindeulemeu  15433  dedekindeu  15434  suplociccreex  15435  dedekindicclemuub  15437  dedekindicclemloc  15439  dedekindicclemlu  15441  dedekindicclemeu  15442  dedekindicclemicc  15443  dedekindicc  15444  ivthinclemlopn  15447  ivthinclemlr  15448  ivthinclemuopn  15449  ivthinclemur  15450  ivthinclemloc  15452  ivthinc  15454  ivthreinc  15456  dich0  15463  ivthdich  15464  limcdifap  15473  limcimolemlt  15475  limccoap  15489  dvlemap  15491  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvcnp2cntop  15510  dvaddxxbr  15512  dvmulxxbr  15513  dvcoapbr  15518  dvcjbr  15519  dvrecap  15524  dveflem  15537  logltb  15685  2irrexpqap  15789  sgmnncl  15802  dvdsppwf1o  15803  mpodvdsmulf1o  15804  perfectlem2  15814  lgsmod  15845  lgsne0  15857  gausslemma2dlem4  15883  2sqlem6  15939  2sqlem8  15942  2sqlem10  15944  upgrm  16041  upgr1or2  16042  umgredg2en  16050  umgrbien  16051  upgr1elem1  16061  umgr1een  16066  edgupgren  16082  edgumgren  16083  umgredgnlp  16093  edgusgren  16104  usgruspgrben  16127  usgr1e  16182  subumgredg2en  16212  subupgr  16214  wlkvtxiedg  16286  wlkvtxiedgg  16287  istrl  16326  iseupth  16388  eupth2fi  16420  konigsberglem1  16429  pw1nct  16725  sbthom  16754  trilpo  16775  trirec0  16776  reap0  16791  cndcap  16792  dcapnconst  16794  neapmkv  16801  neap0mkv  16802  ltlenmkv  16803