Theorem breq1 4007

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

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

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 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005

This theorem is referenced by:  breq12  4009  breq1i  4011  breq1d  4014  nbrne2  4024  brab1  4051  pocl  4304  swopolem  4306  swopo  4307  issod  4320  sowlin  4321  sotritrieq  4326  frirrg  4351  wetriext  4577  vtoclr  4675  brcog  4795  brcogw  4797  opelcnvg  4808  dfdmf  4821  eldmg  4823  dfrnf  4869  dfres2  4960  imasng  4994  coi1  5145  dffun6f  5230  funmo  5232  fun11  5284  fveq2  5516  funfveu  5529  sefvex  5537  nfunsn  5550  fvmptss2  5592  f1ompt  5668  fmptco  5683  dff13  5769  foeqcnvco  5791  isorel  5809  isocnv  5812  isotr  5817  isoini  5819  isopolem  5823  isosolem  5825  f1oiso  5827  f1oiso2  5828  caovordig  6040  caovordg  6042  caovord3d  6045  caovord  6046  caovord3  6048  caofrss  6107  caoftrn  6108  poxp  6233  brtpos2  6252  rntpos  6258  tpostpos  6265  ertr  6550  ecopovsym  6631  ecopovtrn  6632  ecopovsymg  6634  ecopovtrng  6635  th3qlem2  6638  isfi  6761  en0  6795  en1  6799  en1bg  6800  endisj  6824  xpcomco  6826  dom0  6838  ssenen  6851  nneneq  6857  domfiexmid  6878  findcard  6888  findcard2  6889  findcard2s  6890  isinfinf  6897  tridc  6899  fimax2gtrilemstep  6900  fimax2gtri  6901  fiintim  6928  fisseneq  6931  en1eqsnbi  6948  isbth  6966  supmoti  6992  eqsupti  6995  supubti  6998  suplubti  6999  supsnti  7004  isotilem  7005  isoti  7006  supisolem  7007  supisoex  7008  infminti  7026  isnumi  7181  cardval3ex  7184  oncardval  7185  cardonle  7186  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidapne  7259  nqtri3or  7395  ltsonq  7397  ltanqg  7399  ltmnqg  7400  ltexnqq  7407  subhalfnqq  7413  ltbtwnnqq  7414  archnqq  7416  nqnq0pi  7437  prcdnql  7483  prcunqu  7484  prnmaxl  7487  genpcuu  7519  genprndl  7520  genprndu  7521  nqprm  7541  nqprrnd  7542  nqprdisj  7543  nqprloc  7544  nqpru  7551  addnqprlemrl  7556  addnqprlemfl  7558  addnqprlemfu  7559  prmuloc2  7566  mulnqprlemrl  7572  mulnqprlemfl  7574  mulnqprlemfu  7575  1idprl  7589  ltnqpr  7592  ltnqpri  7593  prplnqu  7619  recexprlemell  7621  recexprlemm  7623  recexprlemdisj  7629  recexprlemloc  7630  recexprlem1ssu  7633  recexprlemss1l  7634  aptiprlemu  7639  archpr  7642  cauappcvgprlemm  7644  cauappcvgprlemladdfl  7654  cauappcvgprlem2  7659  cauappcvgpr  7661  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemcl  7675  caucvgprlem2  7679  caucvgpr  7681  caucvgprprlemelu  7685  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemnbj  7692  caucvgprprlemmu  7694  caucvgprprlemopu  7698  caucvgprprlemexbt  7705  caucvgprprlemaddq  7707  caucvgprprlem1  7708  caucvgprprlem2  7709  caucvgprpr  7711  suplocexprlemmu  7717  suplocexprlemloc  7720  suplocexpr  7724  lttrsr  7761  ltsosr  7763  1ne0sr  7765  ltasrg  7769  aptisr  7778  mulextsr1  7780  archsr  7781  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  caucvgsr  7801  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  axpre-ltwlin  7882  axpre-lttrn  7883  axpre-apti  7884  axpre-ltadd  7885  axpre-mulext  7887  axcaucvglemcau  7897  axcaucvglemres  7898  axcaucvg  7899  axpre-suploclemres  7900  axpre-suploc  7901  ltxrlt  8023  lttri3  8037  ltordlem  8439  lt0ne0d  8470  reapti  8536  apreim  8560  apsscn  8604  recexap  8610  lbreu  8902  lble  8904  suprleubex  8911  sup3exmid  8914  nnsub  8958  nominpos  9156  nn0n0n1ge2b  9332  zextle  9344  fzind  9368  btwnz  9372  uzval  9530  supinfneg  9595  infsupneg  9596  infregelbex  9598  ublbneg  9613  lbzbi  9616  qreccl  9642  xrltnsym  9793  xrlttr  9795  xrltso  9796  xrlttri3  9797  nltpnft  9814  npnflt  9815  xrrebnd  9819  xltnegi  9835  xnn0lenn0nn0  9865  xsubge0  9881  xlesubadd  9883  xleaddadd  9887  ixxval  9896  elixx1  9897  elioo2  9921  iccid  9925  fzval  10010  elfz1  10013  qtri3or  10243  exbtwnzlemstep  10248  exbtwnzlemshrink  10249  exbtwnzlemex  10250  exbtwnz  10251  rebtwn2zlemstep  10253  rebtwn2zlemshrink  10254  rebtwn2z  10255  qbtwnre  10257  qbtwnxr  10258  flval  10272  flqlelt  10276  flqbi  10290  flqeqceilz  10318  modqid2  10351  seq3f1olemqsum  10500  seq3f1oleml  10503  seq3f1o  10504  expcl2lemap  10532  expclzaplem  10544  expclzap  10545  expap0i  10552  nn0ltexp2  10689  hashinfuni  10757  hashennnuni  10759  hashunlem  10784  zfz1isolemiso  10819  zfz1isolem1  10820  zfz1iso  10821  absle  11098  maxleast  11222  rexanre  11229  rexico  11230  fimaxre2  11235  minmax  11238  xrmaxltsup  11266  xrminmax  11273  climshft  11312  reccn2ap  11321  summodclem3  11388  summodclem2a  11389  summodc  11391  zsumdc  11392  fsum3  11395  fsum3cvg3  11404  fsumcl2lem  11406  fsumadd  11414  sumsnf  11417  fsummulc2  11456  isumlessdc  11504  cvgratz  11540  mertenslemi1  11543  ntrivcvgap0  11557  prodmodclem3  11583  prodmodclem2a  11584  prodmodc  11586  zproddc  11587  fprodseq  11591  fprodntrivap  11592  fprodmul  11599  prodsnf  11600  absdvdsb  11816  zdvdsdc  11819  dvdsabseq  11853  dvdsdivcl  11856  dvdsext  11861  divalglemnn  11923  divalglemeunn  11926  divalglemeuneg  11928  divalgmod  11932  ndvdssub  11935  zsupcllemstep  11946  suprzubdc  11953  zsupssdc  11955  gcdsupex  11958  gcdsupcl  11959  gcddvds  11964  dvdslegcd  11965  bezoutlemmain  11999  bezoutlemex  12002  bezoutlemzz  12003  bezoutlemmo  12007  bezoutlemeu  12008  bezoutlemle  12009  bezoutlemsup  12010  dfgcd3  12011  dfgcd2  12015  gcdzeq  12023  dvdssq  12032  nnwodc  12037  uzwodc  12038  nnwofdc  12039  nn0seqcvgd  12041  algcvgblem  12049  lcmval  12063  lcmdvds  12079  lcmgcdeq  12083  coprmgcdb  12088  ncoprmgcdne1b  12089  coprmdvds1  12091  1nprm  12114  1idssfct  12115  isprm2lem  12116  isprm2  12117  dvdsprime  12122  nprm  12123  3prm  12128  dvdsprm  12137  exprmfct  12138  isprm5lem  12141  isprm5  12142  coprm  12144  sqrt2irr  12162  phisum  12240  odzval  12241  pythagtriplem4  12268  pc2dvds  12329  pcprmpw2  12332  pcprmpw  12333  dvdsprmpweqle  12336  oddprmdvds  12352  prmpwdvds  12353  pockthg  12355  1arith  12365  exmidunben  12427  nninfdclemcl  12449  nninfdclemp1  12451  nninfdc  12454  imasaddfnlemg  12735  ssblex  13934  comet  14002  bdmopn  14007  reopnap  14041  divcnap  14058  cdivcncfap  14090  cnopnap  14097  dedekindeulemuub  14098  dedekindeulemloc  14100  dedekindeulemlu  14102  dedekindeulemeu  14103  dedekindeu  14104  suplociccreex  14105  dedekindicclemuub  14107  dedekindicclemloc  14109  dedekindicclemlu  14111  dedekindicclemeu  14112  dedekindicclemicc  14113  dedekindicc  14114  ivthinclemlopn  14117  ivthinclemlr  14118  ivthinclemuopn  14119  ivthinclemur  14120  ivthinclemloc  14122  ivthinc  14124  limcdifap  14134  limcimolemlt  14136  limccoap  14150  dvlemap  14152  dvidlemap  14163  dvcnp2cntop  14166  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  dvcjbr  14175  dvrecap  14180  dveflem  14190  logltb  14298  2irrexpqap  14399  lgsmod  14430  lgsne0  14442  2sqlem6  14470  2sqlem8  14473  2sqlem10  14475  pw1nct  14755  sbthom  14777  trilpo  14794  trirec0  14795  reap0  14809  dcapnconst  14811  neapmkv  14818  neap0mkv  14819  ltlenmkv  14820