Theorem breq1 3927

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331   ∈ wcel 1480  ⟨cop 3525   class class class wbr 3924

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-v 2683  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531  df-br 3925

This theorem is referenced by:  breq12  3929  breq1i  3931  breq1d  3934  nbrne2  3943  brab1  3970  pocl  4220  swopolem  4222  swopo  4223  issod  4236  sowlin  4237  sotritrieq  4242  frirrg  4267  wetriext  4486  vtoclr  4582  brcog  4701  brcogw  4703  opelcnvg  4714  dfdmf  4727  eldmg  4729  dfrnf  4775  dfres2  4866  imasng  4899  coi1  5049  dffun6f  5131  funmo  5133  fun11  5185  fveq2  5414  funfveu  5427  sefvex  5435  nfunsn  5448  fvmptss2  5489  f1ompt  5564  fmptco  5579  dff13  5662  foeqcnvco  5684  isorel  5702  isocnv  5705  isotr  5710  isoini  5712  isopolem  5716  isosolem  5718  f1oiso  5720  f1oiso2  5721  caovordig  5929  caovordg  5931  caovord3d  5934  caovord  5935  caovord3  5937  caofrss  5999  caoftrn  6000  poxp  6122  brtpos2  6141  rntpos  6147  tpostpos  6154  ertr  6437  ecopovsym  6518  ecopovtrn  6519  ecopovsymg  6521  ecopovtrng  6522  th3qlem2  6525  isfi  6648  en0  6682  en1  6686  en1bg  6687  endisj  6711  xpcomco  6713  dom0  6725  ssenen  6738  nneneq  6744  domfiexmid  6765  findcard  6775  findcard2  6776  findcard2s  6777  isinfinf  6784  tridc  6786  fimax2gtrilemstep  6787  fimax2gtri  6788  fiintim  6810  fisseneq  6813  en1eqsnbi  6830  isbth  6848  supmoti  6873  eqsupti  6876  supubti  6879  suplubti  6880  supsnti  6885  isotilem  6886  isoti  6887  supisolem  6888  supisoex  6889  infminti  6907  isnumi  7031  cardval3ex  7034  oncardval  7035  cardonle  7036  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  nqtri3or  7197  ltsonq  7199  ltanqg  7201  ltmnqg  7202  ltexnqq  7209  subhalfnqq  7215  ltbtwnnqq  7216  archnqq  7218  nqnq0pi  7239  prcdnql  7285  prcunqu  7286  prnmaxl  7289  genpcuu  7321  genprndl  7322  genprndu  7323  nqprm  7343  nqprrnd  7344  nqprdisj  7345  nqprloc  7346  nqpru  7353  addnqprlemrl  7358  addnqprlemfl  7360  addnqprlemfu  7361  prmuloc2  7368  mulnqprlemrl  7374  mulnqprlemfl  7376  mulnqprlemfu  7377  1idprl  7391  ltnqpr  7394  ltnqpri  7395  prplnqu  7421  recexprlemell  7423  recexprlemm  7425  recexprlemdisj  7431  recexprlemloc  7432  recexprlem1ssu  7435  recexprlemss1l  7436  aptiprlemu  7441  archpr  7444  cauappcvgprlemm  7446  cauappcvgprlemladdfl  7456  cauappcvgprlem2  7461  cauappcvgpr  7463  caucvgprlemnkj  7467  caucvgprlemnbj  7468  caucvgprlemcl  7477  caucvgprlem2  7481  caucvgpr  7483  caucvgprprlemelu  7487  caucvgprprlemcbv  7488  caucvgprprlemval  7489  caucvgprprlemnbj  7494  caucvgprprlemmu  7496  caucvgprprlemopu  7500  caucvgprprlemexbt  7507  caucvgprprlemaddq  7509  caucvgprprlem1  7510  caucvgprprlem2  7511  caucvgprpr  7513  suplocexprlemmu  7519  suplocexprlemloc  7522  suplocexpr  7526  lttrsr  7563  ltsosr  7565  1ne0sr  7567  ltasrg  7571  aptisr  7580  mulextsr1  7582  archsr  7583  caucvgsrlemgt1  7596  caucvgsrlemoffres  7601  caucvgsr  7603  suplocsrlemb  7607  suplocsrlempr  7608  suplocsrlem  7609  axpre-ltwlin  7684  axpre-lttrn  7685  axpre-apti  7686  axpre-ltadd  7687  axpre-mulext  7689  axcaucvglemcau  7699  axcaucvglemres  7700  axcaucvg  7701  axpre-suploclemres  7702  axpre-suploc  7703  ltxrlt  7823  lttri3  7837  ltordlem  8237  lt0ne0d  8268  reapti  8334  apreim  8358  apsscn  8402  recexap  8407  lbreu  8696  lble  8698  suprleubex  8705  sup3exmid  8708  nnsub  8752  nominpos  8950  nn0n0n1ge2b  9123  zextle  9135  fzind  9159  btwnz  9163  uzval  9321  supinfneg  9383  infsupneg  9384  ublbneg  9398  lbzbi  9401  qreccl  9427  xrltnsym  9572  xrlttr  9574  xrltso  9575  xrlttri3  9576  nltpnft  9590  npnflt  9591  xrrebnd  9595  xltnegi  9611  xnn0lenn0nn0  9641  xsubge0  9657  xlesubadd  9659  xleaddadd  9663  ixxval  9672  elixx1  9673  elioo2  9697  iccid  9701  fzval  9785  elfz1  9788  qtri3or  10013  exbtwnzlemstep  10018  exbtwnzlemshrink  10019  exbtwnzlemex  10020  exbtwnz  10021  rebtwn2zlemstep  10023  rebtwn2zlemshrink  10024  rebtwn2z  10025  qbtwnre  10027  qbtwnxr  10028  flval  10038  flqlelt  10042  flqbi  10056  flqeqceilz  10084  modqid2  10117  seq3f1olemqsum  10266  seq3f1oleml  10269  seq3f1o  10270  expcl2lemap  10298  expclzaplem  10310  expclzap  10311  expap0i  10318  hashinfuni  10516  hashennnuni  10518  hashunlem  10543  zfz1isolemiso  10575  zfz1isolem1  10576  zfz1iso  10577  absle  10854  maxleast  10978  rexanre  10985  rexico  10986  fimaxre2  10991  minmax  10994  xrmaxltsup  11020  xrminmax  11027  climshft  11066  reccn2ap  11075  summodclem3  11142  summodclem2a  11143  summodc  11145  zsumdc  11146  fsum3  11149  fsum3cvg3  11158  fsumcl2lem  11160  fsumadd  11168  sumsnf  11171  fsummulc2  11210  isumlessdc  11258  cvgratz  11294  mertenslemi1  11297  ntrivcvgap0  11311  absdvdsb  11500  zdvdsdc  11503  dvdsabseq  11534  dvdsdivcl  11537  dvdsext  11542  divalglemnn  11604  divalglemeunn  11607  divalglemeuneg  11609  divalgmod  11613  ndvdssub  11616  zsupcllemstep  11627  gcdsupex  11635  gcdsupcl  11636  gcddvds  11641  dvdslegcd  11642  bezoutlemmain  11675  bezoutlemex  11678  bezoutlemzz  11679  bezoutlemmo  11683  bezoutlemeu  11684  bezoutlemle  11685  bezoutlemsup  11686  dfgcd3  11687  dfgcd2  11691  gcdzeq  11699  dvdssq  11708  nn0seqcvgd  11711  algcvgblem  11719  lcmval  11733  lcmdvds  11749  lcmgcdeq  11753  coprmgcdb  11758  ncoprmgcdne1b  11759  coprmdvds1  11761  1nprm  11784  1idssfct  11785  isprm2lem  11786  isprm2  11787  dvdsprime  11792  nprm  11793  3prm  11798  dvdsprm  11806  exprmfct  11807  coprm  11811  sqrt2irr  11829  exmidunben  11928  ssblex  12589  comet  12657  bdmopn  12662  reopnap  12696  divcnap  12713  cdivcncfap  12745  cnopnap  12752  dedekindeulemuub  12753  dedekindeulemloc  12755  dedekindeulemlu  12757  dedekindeulemeu  12758  dedekindeu  12759  suplociccreex  12760  dedekindicclemuub  12762  dedekindicclemloc  12764  dedekindicclemlu  12766  dedekindicclemeu  12767  dedekindicclemicc  12768  dedekindicc  12769  ivthinclemlopn  12772  ivthinclemlr  12773  ivthinclemuopn  12774  ivthinclemur  12775  ivthinclemloc  12777  ivthinc  12779  limcdifap  12789  limcimolemlt  12791  limccoap  12805  dvlemap  12807  dvidlemap  12818  dvcnp2cntop  12821  dvaddxxbr  12823  dvmulxxbr  12824  dvcoapbr  12829  dvcjbr  12830  dvrecap  12835  dveflem  12844  sbthom  13210  trilpo  13225