Theorem breq1 4062

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ wcel 2178  ⟨cop 3646   class class class wbr 4059

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060

This theorem is referenced by:  breq12  4064  breq1i  4066  breq1d  4069  nbrne2  4079  brab1  4107  pocl  4368  swopolem  4370  swopo  4371  issod  4384  sowlin  4385  sotritrieq  4390  frirrg  4415  wetriext  4643  vtoclr  4741  brcog  4863  brcogw  4865  opelcnvg  4876  dfdmf  4890  eldmg  4892  dfrnf  4938  dfres2  5030  imasng  5066  coi1  5217  dffun6f  5303  funmo  5305  fun11  5360  fveq2  5599  funfveu  5612  sefvex  5620  nfunsn  5634  fvmptss2  5677  f1ompt  5754  fmptco  5769  dff13  5860  foeqcnvco  5882  isorel  5900  isocnv  5903  isotr  5908  isoini  5910  isopolem  5914  isosolem  5916  f1oiso  5918  f1oiso2  5919  caovordig  6135  caovordg  6137  caovord3d  6140  caovord  6141  caovord3  6143  caofrss  6213  caoftrn  6214  poxp  6341  brtpos2  6360  rntpos  6366  tpostpos  6373  ertr  6658  ecopovsym  6741  ecopovtrn  6742  ecopovsymg  6744  ecopovtrng  6745  th3qlem2  6748  isfi  6875  en0  6910  en1  6914  en1bg  6915  endisj  6944  xpcomco  6946  dom0  6960  ssenen  6973  nneneq  6979  domfiexmid  7001  findcard  7011  findcard2  7012  findcard2s  7013  isinfinf  7020  tridc  7022  fimax2gtrilemstep  7023  fimax2gtri  7024  fiintim  7054  fisseneq  7057  en1eqsnbi  7077  isbth  7095  supmoti  7121  eqsupti  7124  supubti  7127  suplubti  7128  supsnti  7133  isotilem  7134  isoti  7135  supisolem  7136  supisoex  7137  infminti  7155  isnumi  7315  cardval3ex  7318  oncardval  7319  cardonle  7320  en2prde  7327  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidapne  7407  nqtri3or  7544  ltsonq  7546  ltanqg  7548  ltmnqg  7549  ltexnqq  7556  subhalfnqq  7562  ltbtwnnqq  7563  archnqq  7565  nqnq0pi  7586  prcdnql  7632  prcunqu  7633  prnmaxl  7636  genpcuu  7668  genprndl  7669  genprndu  7670  nqprm  7690  nqprrnd  7691  nqprdisj  7692  nqprloc  7693  nqpru  7700  addnqprlemrl  7705  addnqprlemfl  7707  addnqprlemfu  7708  prmuloc2  7715  mulnqprlemrl  7721  mulnqprlemfl  7723  mulnqprlemfu  7724  1idprl  7738  ltnqpr  7741  ltnqpri  7742  prplnqu  7768  recexprlemell  7770  recexprlemm  7772  recexprlemdisj  7778  recexprlemloc  7779  recexprlem1ssu  7782  recexprlemss1l  7783  aptiprlemu  7788  archpr  7791  cauappcvgprlemm  7793  cauappcvgprlemladdfl  7803  cauappcvgprlem2  7808  cauappcvgpr  7810  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemcl  7824  caucvgprlem2  7828  caucvgpr  7830  caucvgprprlemelu  7834  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemnbj  7841  caucvgprprlemmu  7843  caucvgprprlemopu  7847  caucvgprprlemexbt  7854  caucvgprprlemaddq  7856  caucvgprprlem1  7857  caucvgprprlem2  7858  caucvgprpr  7860  suplocexprlemmu  7866  suplocexprlemloc  7869  suplocexpr  7873  lttrsr  7910  ltsosr  7912  1ne0sr  7914  ltasrg  7918  aptisr  7927  mulextsr1  7929  archsr  7930  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  caucvgsr  7950  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  axpre-ltwlin  8031  axpre-lttrn  8032  axpre-apti  8033  axpre-ltadd  8034  axpre-mulext  8036  axcaucvglemcau  8046  axcaucvglemres  8047  axcaucvg  8048  axpre-suploclemres  8049  axpre-suploc  8050  ltxrlt  8173  lttri3  8187  ltordlem  8590  lt0ne0d  8621  reapti  8687  apreim  8711  apsscn  8755  recexap  8761  lbreu  9053  lble  9055  suprleubex  9062  sup3exmid  9065  nnsub  9110  nominpos  9310  nn0n0n1ge2b  9487  zextle  9499  fzind  9523  btwnz  9527  uzval  9685  supinfneg  9751  infsupneg  9752  infregelbex  9754  ublbneg  9769  lbzbi  9772  qreccl  9798  xrltnsym  9950  xrlttr  9952  xrltso  9953  xrlttri3  9954  nltpnft  9971  npnflt  9972  xrrebnd  9976  xltnegi  9992  xnn0lenn0nn0  10022  xsubge0  10038  xlesubadd  10040  xleaddadd  10044  ixxval  10053  elixx1  10054  elioo2  10078  iccid  10082  fzval  10167  elfz1  10170  zsupcllemstep  10409  suprzubdc  10416  zsupssdc  10418  qtri3or  10420  exbtwnzlemstep  10427  exbtwnzlemshrink  10428  exbtwnzlemex  10429  exbtwnz  10430  rebtwn2zlemstep  10432  rebtwn2zlemshrink  10433  rebtwn2z  10434  qbtwnre  10436  qbtwnxr  10437  flval  10452  flqlelt  10456  flqbi  10470  flqeqceilz  10500  modqid2  10533  seq3f1olemqsum  10695  seq3f1oleml  10698  seq3f1o  10699  seqf1oglem2  10702  expcl2lemap  10733  expclzaplem  10745  expclzap  10746  expap0i  10753  nn0ltexp2  10891  hashinfuni  10959  hashennnuni  10961  hashunlem  10986  zfz1isolemiso  11021  zfz1isolem1  11022  zfz1iso  11023  absle  11515  maxleast  11639  rexanre  11646  rexico  11647  fimaxre2  11653  minmax  11656  xrmaxltsup  11684  xrminmax  11691  climshft  11730  reccn2ap  11739  summodclem3  11806  summodclem2a  11807  summodc  11809  zsumdc  11810  fsum3  11813  fsum3cvg3  11822  fsumcl2lem  11824  fsumadd  11832  sumsnf  11835  fsummulc2  11874  isumlessdc  11922  cvgratz  11958  mertenslemi1  11961  ntrivcvgap0  11975  prodmodclem3  12001  prodmodclem2a  12002  prodmodc  12004  zproddc  12005  fprodseq  12009  fprodntrivap  12010  fprodmul  12017  prodsnf  12018  absdvdsb  12235  zdvdsdc  12238  dvdsabseq  12273  dvdsdivcl  12276  dvdsext  12281  divalglemnn  12344  divalglemeunn  12347  divalglemeuneg  12349  divalgmod  12353  ndvdssub  12356  gcdsupex  12393  gcdsupcl  12394  gcddvds  12399  dvdslegcd  12400  bezoutlemmain  12434  bezoutlemex  12437  bezoutlemzz  12438  bezoutlemmo  12442  bezoutlemeu  12443  bezoutlemle  12444  bezoutlemsup  12445  dfgcd3  12446  dfgcd2  12450  gcdzeq  12458  dvdssq  12467  nnwodc  12472  uzwodc  12473  nnwofdc  12474  nn0seqcvgd  12478  algcvgblem  12486  lcmval  12500  lcmdvds  12516  lcmgcdeq  12520  coprmgcdb  12525  ncoprmgcdne1b  12526  coprmdvds1  12528  1nprm  12551  1idssfct  12552  isprm2lem  12553  isprm2  12554  dvdsprime  12559  nprm  12560  3prm  12565  dvdsprm  12574  exprmfct  12575  isprm5lem  12578  isprm5  12579  coprm  12581  sqrt2irr  12599  dvdsfi  12676  phisum  12678  odzval  12679  pythagtriplem4  12706  pc2dvds  12768  pcprmpw2  12771  pcprmpw  12772  dvdsprmpweqle  12775  oddprmdvds  12792  prmpwdvds  12793  pockthg  12795  1arith  12805  exmidunben  12912  nninfdclemcl  12934  nninfdclemp1  12936  nninfdc  12939  imasaddfnlemg  13261  cnfldui  14466  znleval  14530  ssblex  15018  comet  15086  bdmopn  15091  reopnap  15133  divcnap  15152  cdivcncfap  15191  cnopnap  15198  divcncfap  15201  maxcncf  15202  mincncf  15203  dedekindeulemuub  15204  dedekindeulemloc  15206  dedekindeulemlu  15208  dedekindeulemeu  15209  dedekindeu  15210  suplociccreex  15211  dedekindicclemuub  15213  dedekindicclemloc  15215  dedekindicclemlu  15217  dedekindicclemeu  15218  dedekindicclemicc  15219  dedekindicc  15220  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemloc  15228  ivthinc  15230  ivthreinc  15232  dich0  15239  ivthdich  15240  limcdifap  15249  limcimolemlt  15251  limccoap  15265  dvlemap  15267  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvcnp2cntop  15286  dvaddxxbr  15288  dvmulxxbr  15289  dvcoapbr  15294  dvcjbr  15295  dvrecap  15300  dveflem  15313  logltb  15461  2irrexpqap  15565  sgmnncl  15575  dvdsppwf1o  15576  mpodvdsmulf1o  15577  perfectlem2  15587  lgsmod  15618  lgsne0  15630  gausslemma2dlem4  15656  2sqlem6  15712  2sqlem8  15715  2sqlem10  15717  upgrm  15811  upgr1or2  15812  umgredg2en  15820  umgrbien  15821  upgr1elem1  15828  edgupgren  15845  edgumgren  15846  umgredgnlp  15856  pw1nct  16142  sbthom  16167  trilpo  16184  trirec0  16185  reap0  16199  cndcap  16200  dcapnconst  16202  neapmkv  16209  neap0mkv  16210  ltlenmkv  16211