Theorem breq2 4037

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2167  ⟨cop 3625   class class class wbr 4033

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034

This theorem is referenced by:  breq12  4038  breq2i  4041  breq2d  4045  nbrne1  4052  brralrspcev  4091  brimralrspcev  4092  pocl  4338  swopolem  4340  swopo  4341  sowlin  4355  sotricim  4358  sotritrieq  4360  seex  4370  frind  4387  wetriext  4613  vtoclr  4711  posng  4735  brcog  4833  brcogw  4835  opelcnvg  4846  dfdmf  4859  breldmg  4872  dfrnf  4907  dmcoss  4935  resieq  4956  dfres2  4998  elimag  5013  elrelimasn  5035  elimasn  5036  intirr  5056  poirr2  5062  poltletr  5070  dffun6f  5271  dffun4f  5274  fun11  5325  brprcneu  5551  fv3  5581  tz6.12c  5588  relelfvdm  5590  funbrfv  5599  fnbrfvb  5601  funfvdm2f  5626  fndmdif  5667  dff3im  5707  fmptco  5728  foeqcnvco  5837  isorel  5855  isocnv  5858  isotr  5863  isopolem  5869  isosolem  5871  f1oiso  5873  f1oiso2  5874  caovordig  6089  caovordg  6091  caovord  6095  caofrss  6162  caoftrn  6163  poxp  6290  tposoprab  6338  ertr  6607  ecopovsym  6690  ecopovtrn  6691  ecopovsymg  6693  ecopovtrng  6694  th3qlem2  6697  domeng  6811  eqeng  6825  snfig  6873  nneneq  6918  nnfi  6933  ssfilem  6936  domfiexmid  6939  dif1enen  6941  diffitest  6948  findcard  6949  findcard2  6950  findcard2s  6951  diffisn  6954  tridc  6960  fimax2gtrilemstep  6961  inffiexmid  6967  unsnfi  6980  fiintim  6992  fisseneq  6995  isbth  7033  supmoti  7059  eqsupti  7062  supubti  7065  suplubti  7066  suplub2ti  7067  supmaxti  7070  supsnti  7071  isotilem  7072  isoti  7073  supisolem  7074  supisoex  7075  cardcl  7248  isnumi  7249  cardval3ex  7252  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidapne  7327  nqtri3or  7463  ltsonq  7465  ltanqg  7467  ltmnqg  7468  ltexnqq  7475  nsmallnqq  7479  subhalfnqq  7481  ltbtwnnqq  7482  prarloclemarch2  7486  nqnq0pi  7505  prcdnql  7551  prcunqu  7552  prnminu  7556  genpcdl  7586  genprndl  7588  genprndu  7589  genpdisj  7590  nqprm  7609  nqprrnd  7610  nqprdisj  7611  nqprloc  7612  nqprlu  7614  nqprl  7618  addnqprlemru  7625  addnqprlemfl  7626  addnqprlemfu  7627  mulnqprlemru  7641  mulnqprlemfl  7642  mulnqprlemfu  7643  1idpru  7658  ltnqpr  7660  ltnqpri  7661  prplnqu  7687  recexprlemelu  7690  recexprlemm  7691  recexprlemloc  7698  recexprlem1ssl  7700  recexprlemss1u  7703  cauappcvgprlemm  7712  cauappcvgprlemopu  7715  cauappcvgprlemupu  7716  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdfu  7721  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem2  7727  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemopu  7738  caucvgprlemupu  7739  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemcl  7743  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlem2  7747  caucvgprprlemelu  7753  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemnbj  7760  caucvgprprlemmu  7762  caucvgprprlemexbt  7773  caucvgprprlemaddq  7775  caucvgprprlem1  7776  caucvgprprlem2  7777  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  suplocexpr  7792  lttrsr  7829  ltsosr  7831  ltasrg  7837  recexgt0sr  7840  mulgt0sr  7845  aptisr  7846  mulextsr1  7848  srpospr  7850  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  caucvgsr  7869  map2psrprg  7872  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  axprecex  7947  axpre-ltwlin  7950  axpre-lttrn  7951  axpre-apti  7952  axpre-ltadd  7953  axpre-mulgt0  7954  axpre-mulext  7955  axcaucvglemcau  7965  axcaucvglemres  7966  axcaucvg  7967  axpre-suploclemres  7968  axpre-suploc  7969  ltxrlt  8092  lttri3  8106  ltne  8111  eqle  8118  ltordlem  8509  reapti  8606  apreim  8630  squeeze0  8931  lbreu  8972  lble  8974  suprleubex  8981  sup3exmid  8984  nnge1  9013  nn2ge  9023  nn1gt1  9024  nnsub  9029  nominpos  9229  nn0ge0  9274  elnnnn0b  9293  nn0ge2m1nn  9309  zdclt  9403  suprzclex  9424  peano2uz2  9433  peano5uzti  9434  dfuzi  9436  uzind  9437  uzind3  9439  eluz1  9605  uzind4  9662  indstr  9667  supinfneg  9669  infsupneg  9670  infregelbex  9672  indstr2  9683  ublbneg  9687  irrmulap  9722  elpq  9723  elpqb  9724  elrp  9730  mnfltxr  9861  nn0pnfge0  9866  xrltnsym  9868  xrlttr  9870  xrltso  9871  xrlttri3  9872  xrltne  9888  ngtmnft  9892  nmnfgt  9893  xrrebnd  9894  z2ge  9901  xltnegi  9910  xltadd1  9951  xsubge0  9956  xleaddadd  9962  ixxval  9971  elixx1  9972  elioo2  9996  iccid  10000  iccsupr  10041  repos  10045  fzval  10085  elfz1  10088  fzm1  10175  zsupcllemstep  10319  suprzubdc  10326  zsupssdc  10328  qdclt  10335  exbtwnzlemstep  10337  exbtwnzlemex  10339  qbtwnre  10346  qbtwnxr  10347  flval  10362  apbtwnz  10364  modqid2  10443  modqmuladdnn0  10460  exp3val  10633  expge0  10667  expge1  10668  nn0ltexp2  10801  facdiv  10830  facwordi  10832  hashinfom  10870  hashennn  10872  hashunlem  10896  zfz1iso  10933  wrdlen1  10972  fstwrdne0  10974  ovshftex  10984  shftfibg  10985  shftfib  10988  shftfn  10989  2shfti  10996  sqrt0rlem  11168  resqrexlemex  11190  rsqrmo  11192  resqrtcl  11194  rersqrtthlem  11195  sqrtsq  11209  cau3lem  11279  caubnd2  11282  maxleim  11370  maxabslemval  11373  maxleast  11378  maxleb  11381  fimaxre2  11392  minmax  11395  xrmaxleim  11409  xrmaxiflemval  11415  xrmaxaddlem  11425  xrminmax  11430  xrbdtri  11441  climi  11452  climeu  11461  climmo  11463  2clim  11466  addcn2  11475  mulcn2  11477  reccn2ap  11478  cn1lem  11479  summodc  11548  zsumdc  11549  fsum3  11552  cvgratz  11697  ntrivcvgap0  11714  prodmodc  11743  zproddc  11744  fprodseq  11748  fprodntrivap  11749  sinltxirr  11926  dvdsabsb  11975  0dvds  11976  alzdvds  12019  dvdsext  12020  fzo0dvdseq  12022  2tp1odd  12049  2teven  12052  divalglemnn  12083  divalglemeunn  12086  divalglemeuneg  12088  gcdval  12126  gcddvds  12130  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlemex  12168  bezoutlemeu  12174  bezoutlemsup  12176  dfgcd3  12177  bezout  12178  dvdsgcd  12179  dfgcd2  12181  dvdssq  12198  uzwodc  12204  nnwofdc  12205  lcmval  12231  lcmcllem  12235  dvdslcm  12237  lcmledvds  12238  lcmgcdlem  12245  lcmdvds  12247  coprmgcdb  12256  coprmdvds2  12261  cncongr1  12271  cncongr2  12272  isprm  12277  dvdsnprmd  12293  dvdsprm  12305  exprmfct  12306  isprm6  12315  prmexpb  12319  prmfac1  12320  rpexp  12321  sqrt2irr  12330  oddpwdclemdc  12341  oddpwdc  12342  sqpweven  12343  2sqpwodd  12344  sqne2sq  12345  nnoddn2prmb  12431  pceu  12464  pczpre  12466  pcdiv  12471  pcdvdsb  12489  difsqpwdvds  12507  pcmpt  12512  pcmptdvds  12514  oddprmdvds  12523  prmpwdvds  12524  infpnlem2  12529  oddennn  12609  evenennn  12610  exmidunben  12643  nninfdclemcl  12665  nninfdclemp1  12667  nninfdc  12670  infpn2  12673  eqgen  13357  zndvds  14205  znleval  14209  comet  14735  metcnpi  14751  metcnpi2  14752  metcnpi3  14753  addcncntoplem  14797  cncfi  14814  elcncf1di  14815  mulcncflem  14843  dedekindeulemuub  14853  dedekindeulemloc  14855  dedekindeulemlu  14857  dedekindeulemeu  14858  dedekindeu  14859  suplociccreex  14860  suplociccex  14861  dedekindicclemuub  14862  dedekindicclemloc  14864  dedekindicclemlu  14866  dedekindicclemeu  14867  dedekindicclemicc  14868  dedekindicc  14869  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemloc  14877  ivthinc  14879  ivthreinc  14881  dich0  14888  ivthdich  14889  limcimo  14901  cnplimclemr  14905  limccnp2lem  14912  limccoap  14914  eldvap  14918  logltb  15110  lgsdir  15276  lgsne0  15279  gausslemma2dlem0i  15298  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  2lgslem2  15333  2lgs  15345  2sqlem6  15361  2sqlem8  15364  2sqlem10  15366  sbthom  15670  trilpo  15687  trirec0  15688  apdiff  15692  reap0  15702  cndcap  15703  nconstwlpolem  15709  neapmkv  15712  neap0mkv  15713  ltlenmkv  15714