Theorem breq2 3980

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
breq2	⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 3753	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	eleq1d 2233	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3		df-br 3977	. 2 ⊢ (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4		df-br 3977	. 2 ⊢ (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 222	1 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1342   ∈ wcel 2135  ⟨cop 3573   class class class wbr 3976

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 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579  df-br 3977

This theorem is referenced by:  breq12  3981  breq2i  3984  breq2d  3988  nbrne1  3995  brralrspcev  4034  brimralrspcev  4035  pocl  4275  swopolem  4277  swopo  4278  sowlin  4292  sotricim  4295  sotritrieq  4297  seex  4307  frind  4324  wetriext  4548  vtoclr  4646  posng  4670  brcog  4765  brcogw  4767  opelcnvg  4778  dfdmf  4791  breldmg  4804  dfrnf  4839  dmcoss  4867  resieq  4888  dfres2  4930  elimag  4944  elreimasng  4964  elimasn  4965  intirr  4984  poirr2  4990  poltletr  4998  dffun6f  5195  dffun4f  5198  fun11  5249  brprcneu  5473  fv3  5503  tz6.12c  5510  relelfvdm  5512  funbrfv  5519  fnbrfvb  5521  funfvdm2f  5545  fndmdif  5584  dff3im  5624  fmptco  5645  foeqcnvco  5752  isorel  5770  isocnv  5773  isotr  5778  isopolem  5784  isosolem  5786  f1oiso  5788  f1oiso2  5789  caovordig  5998  caovordg  6000  caovord  6004  caofrss  6068  caoftrn  6069  poxp  6191  tposoprab  6239  ertr  6507  ecopovsym  6588  ecopovtrn  6589  ecopovsymg  6591  ecopovtrng  6592  th3qlem2  6595  domeng  6709  eqeng  6723  snfig  6771  nneneq  6814  nnfi  6829  ssfilem  6832  domfiexmid  6835  dif1enen  6837  diffitest  6844  findcard  6845  findcard2  6846  findcard2s  6847  diffisn  6850  tridc  6856  fimax2gtrilemstep  6857  inffiexmid  6863  unsnfi  6875  fiintim  6885  fisseneq  6888  isbth  6923  supmoti  6949  eqsupti  6952  supubti  6955  suplubti  6956  suplub2ti  6957  supmaxti  6960  supsnti  6961  isotilem  6962  isoti  6963  supisolem  6964  supisoex  6965  cardcl  7128  isnumi  7129  cardval3ex  7132  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  nqtri3or  7328  ltsonq  7330  ltanqg  7332  ltmnqg  7333  ltexnqq  7340  nsmallnqq  7344  subhalfnqq  7346  ltbtwnnqq  7347  prarloclemarch2  7351  nqnq0pi  7370  prcdnql  7416  prcunqu  7417  prnminu  7421  genpcdl  7451  genprndl  7453  genprndu  7454  genpdisj  7455  nqprm  7474  nqprrnd  7475  nqprdisj  7476  nqprloc  7477  nqprlu  7479  nqprl  7483  addnqprlemru  7490  addnqprlemfl  7491  addnqprlemfu  7492  mulnqprlemru  7506  mulnqprlemfl  7507  mulnqprlemfu  7508  1idpru  7523  ltnqpr  7525  ltnqpri  7526  prplnqu  7552  recexprlemelu  7555  recexprlemm  7556  recexprlemloc  7563  recexprlem1ssl  7565  recexprlemss1u  7568  cauappcvgprlemm  7577  cauappcvgprlemopu  7580  cauappcvgprlemupu  7581  cauappcvgprlemdisj  7583  cauappcvgprlemloc  7584  cauappcvgprlemladdfu  7586  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  cauappcvgprlem2  7592  caucvgprlemnkj  7598  caucvgprlemnbj  7599  caucvgprlemm  7600  caucvgprlemopu  7603  caucvgprlemupu  7604  caucvgprlemdisj  7606  caucvgprlemloc  7607  caucvgprlemcl  7608  caucvgprlemladdfu  7609  caucvgprlemladdrl  7610  caucvgprlem2  7612  caucvgprprlemelu  7618  caucvgprprlemcbv  7619  caucvgprprlemval  7620  caucvgprprlemnbj  7625  caucvgprprlemmu  7627  caucvgprprlemexbt  7638  caucvgprprlemaddq  7640  caucvgprprlem1  7641  caucvgprprlem2  7642  suplocexprlemmu  7650  suplocexprlemru  7651  suplocexprlemdisj  7652  suplocexprlemloc  7653  suplocexprlemub  7655  suplocexpr  7657  lttrsr  7694  ltsosr  7696  ltasrg  7702  recexgt0sr  7705  mulgt0sr  7710  aptisr  7711  mulextsr1  7713  srpospr  7715  caucvgsrlemgt1  7727  caucvgsrlemoffres  7732  caucvgsr  7734  map2psrprg  7737  suplocsrlemb  7738  suplocsrlempr  7739  suplocsrlem  7740  axprecex  7812  axpre-ltwlin  7815  axpre-lttrn  7816  axpre-apti  7817  axpre-ltadd  7818  axpre-mulgt0  7819  axpre-mulext  7820  axcaucvglemcau  7830  axcaucvglemres  7831  axcaucvg  7832  axpre-suploclemres  7833  axpre-suploc  7834  ltxrlt  7955  lttri3  7969  ltne  7974  eqle  7981  ltordlem  8371  reapti  8468  apreim  8492  squeeze0  8790  lbreu  8831  lble  8833  suprleubex  8840  sup3exmid  8843  nnge1  8871  nn2ge  8881  nn1gt1  8882  nnsub  8887  nominpos  9085  nn0ge0  9130  elnnnn0b  9149  nn0ge2m1nn  9165  zdclt  9259  suprzclex  9280  peano2uz2  9289  peano5uzti  9290  dfuzi  9292  uzind  9293  uzind3  9295  eluz1  9461  uzind4  9517  indstr  9522  supinfneg  9524  infsupneg  9525  infregelbex  9527  indstr2  9538  ublbneg  9542  elpq  9577  elpqb  9578  elrp  9582  mnfltxr  9713  nn0pnfge0  9718  xrltnsym  9720  xrlttr  9722  xrltso  9723  xrlttri3  9724  xrltne  9740  ngtmnft  9744  nmnfgt  9745  xrrebnd  9746  z2ge  9753  xltnegi  9762  xltadd1  9803  xsubge0  9808  xleaddadd  9814  ixxval  9823  elixx1  9824  elioo2  9848  iccid  9852  iccsupr  9893  repos  9897  fzval  9937  elfz1  9940  fzm1  10025  exbtwnzlemstep  10173  exbtwnzlemex  10175  qbtwnre  10182  qbtwnxr  10183  flval  10197  apbtwnz  10199  modqid2  10276  modqmuladdnn0  10293  exp3val  10447  expge0  10481  expge1  10482  nn0ltexp2  10612  facdiv  10640  facwordi  10642  hashinfom  10680  hashennn  10682  hashunlem  10706  zfz1iso  10740  ovshftex  10747  shftfibg  10748  shftfib  10751  shftfn  10752  2shfti  10759  sqrt0rlem  10931  resqrexlemex  10953  rsqrmo  10955  resqrtcl  10957  rersqrtthlem  10958  sqrtsq  10972  cau3lem  11042  caubnd2  11045  maxleim  11133  maxabslemval  11136  maxleast  11141  maxleb  11144  fimaxre2  11154  minmax  11157  xrmaxleim  11171  xrmaxiflemval  11177  xrmaxaddlem  11187  xrminmax  11192  xrbdtri  11203  climi  11214  climeu  11223  climmo  11225  2clim  11228  addcn2  11237  mulcn2  11239  reccn2ap  11240  cn1lem  11241  summodc  11310  zsumdc  11311  fsum3  11314  cvgratz  11459  ntrivcvgap0  11476  prodmodc  11505  zproddc  11506  fprodseq  11510  fprodntrivap  11511  dvdsabsb  11736  0dvds  11737  alzdvds  11777  dvdsext  11778  fzo0dvdseq  11780  2tp1odd  11806  2teven  11809  divalglemnn  11840  divalglemeunn  11843  divalglemeuneg  11845  zsupcllemstep  11863  suprzubdc  11870  zsupssdc  11872  gcdval  11877  gcddvds  11881  bezoutlemstep  11915  bezoutlemmain  11916  bezoutlemex  11919  bezoutlemeu  11925  bezoutlemsup  11927  dfgcd3  11928  bezout  11929  dvdsgcd  11930  dfgcd2  11932  dvdssq  11949  lcmval  11974  lcmcllem  11978  dvdslcm  11980  lcmledvds  11981  lcmgcdlem  11988  lcmdvds  11990  coprmgcdb  11999  coprmdvds2  12004  cncongr1  12014  cncongr2  12015  isprm  12020  dvdsnprmd  12036  dvdsprm  12048  exprmfct  12049  isprm6  12056  prmexpb  12060  prmfac1  12061  rpexp  12062  sqrt2irr  12071  oddpwdclemdc  12082  oddpwdc  12083  sqpweven  12084  2sqpwodd  12085  sqne2sq  12086  nnoddn2prmb  12171  pceu  12204  pczpre  12206  pcdiv  12211  pcdvdsb  12228  difsqpwdvds  12246  pcmpt  12250  pcmptdvds  12252  oddprmdvds  12261  oddennn  12262  evenennn  12263  exmidunben  12296  nninfdclemcl  12320  nninfdclemp1  12322  nninfdc  12325  comet  13040  metcnpi  13056  metcnpi2  13057  metcnpi3  13058  addcncntoplem  13092  cncfi  13106  elcncf1di  13107  mulcncflem  13131  dedekindeulemuub  13136  dedekindeulemloc  13138  dedekindeulemlu  13140  dedekindeulemeu  13141  dedekindeu  13142  suplociccreex  13143  suplociccex  13144  dedekindicclemuub  13145  dedekindicclemloc  13147  dedekindicclemlu  13149  dedekindicclemeu  13150  dedekindicclemicc  13151  dedekindicc  13152  ivthinclemlopn  13155  ivthinclemlr  13156  ivthinclemuopn  13157  ivthinclemur  13158  ivthinclemloc  13160  ivthinc  13162  limcimo  13175  cnplimclemr  13179  limccnp2lem  13186  limccoap  13188  eldvap  13192  logltb  13336  sbthom  13739  trilpo  13756  trirec0  13757  apdiff  13761  reap0  13771  nconstwlpolem  13777  neapmkv  13780