Theorem breq2 3986

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1343   ∈ wcel 2136  ⟨cop 3579   class class class wbr 3982

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-br 3983

This theorem is referenced by:  breq12  3987  breq2i  3990  breq2d  3994  nbrne1  4001  brralrspcev  4040  brimralrspcev  4041  pocl  4281  swopolem  4283  swopo  4284  sowlin  4298  sotricim  4301  sotritrieq  4303  seex  4313  frind  4330  wetriext  4554  vtoclr  4652  posng  4676  brcog  4771  brcogw  4773  opelcnvg  4784  dfdmf  4797  breldmg  4810  dfrnf  4845  dmcoss  4873  resieq  4894  dfres2  4936  elimag  4950  elreimasng  4970  elimasn  4971  intirr  4990  poirr2  4996  poltletr  5004  dffun6f  5201  dffun4f  5204  fun11  5255  brprcneu  5479  fv3  5509  tz6.12c  5516  relelfvdm  5518  funbrfv  5525  fnbrfvb  5527  funfvdm2f  5551  fndmdif  5590  dff3im  5630  fmptco  5651  foeqcnvco  5758  isorel  5776  isocnv  5779  isotr  5784  isopolem  5790  isosolem  5792  f1oiso  5794  f1oiso2  5795  caovordig  6007  caovordg  6009  caovord  6013  caofrss  6074  caoftrn  6075  poxp  6200  tposoprab  6248  ertr  6516  ecopovsym  6597  ecopovtrn  6598  ecopovsymg  6600  ecopovtrng  6601  th3qlem2  6604  domeng  6718  eqeng  6732  snfig  6780  nneneq  6823  nnfi  6838  ssfilem  6841  domfiexmid  6844  dif1enen  6846  diffitest  6853  findcard  6854  findcard2  6855  findcard2s  6856  diffisn  6859  tridc  6865  fimax2gtrilemstep  6866  inffiexmid  6872  unsnfi  6884  fiintim  6894  fisseneq  6897  isbth  6932  supmoti  6958  eqsupti  6961  supubti  6964  suplubti  6965  suplub2ti  6966  supmaxti  6969  supsnti  6970  isotilem  6971  isoti  6972  supisolem  6973  supisoex  6974  cardcl  7137  isnumi  7138  cardval3ex  7141  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  nqtri3or  7337  ltsonq  7339  ltanqg  7341  ltmnqg  7342  ltexnqq  7349  nsmallnqq  7353  subhalfnqq  7355  ltbtwnnqq  7356  prarloclemarch2  7360  nqnq0pi  7379  prcdnql  7425  prcunqu  7426  prnminu  7430  genpcdl  7460  genprndl  7462  genprndu  7463  genpdisj  7464  nqprm  7483  nqprrnd  7484  nqprdisj  7485  nqprloc  7486  nqprlu  7488  nqprl  7492  addnqprlemru  7499  addnqprlemfl  7500  addnqprlemfu  7501  mulnqprlemru  7515  mulnqprlemfl  7516  mulnqprlemfu  7517  1idpru  7532  ltnqpr  7534  ltnqpri  7535  prplnqu  7561  recexprlemelu  7564  recexprlemm  7565  recexprlemloc  7572  recexprlem1ssl  7574  recexprlemss1u  7577  cauappcvgprlemm  7586  cauappcvgprlemopu  7589  cauappcvgprlemupu  7590  cauappcvgprlemdisj  7592  cauappcvgprlemloc  7593  cauappcvgprlemladdfu  7595  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgprlem2  7601  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemm  7609  caucvgprlemopu  7612  caucvgprlemupu  7613  caucvgprlemdisj  7615  caucvgprlemloc  7616  caucvgprlemcl  7617  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  caucvgprlem2  7621  caucvgprprlemelu  7627  caucvgprprlemcbv  7628  caucvgprprlemval  7629  caucvgprprlemnbj  7634  caucvgprprlemmu  7636  caucvgprprlemexbt  7647  caucvgprprlemaddq  7649  caucvgprprlem1  7650  caucvgprprlem2  7651  suplocexprlemmu  7659  suplocexprlemru  7660  suplocexprlemdisj  7661  suplocexprlemloc  7662  suplocexprlemub  7664  suplocexpr  7666  lttrsr  7703  ltsosr  7705  ltasrg  7711  recexgt0sr  7714  mulgt0sr  7719  aptisr  7720  mulextsr1  7722  srpospr  7724  caucvgsrlemgt1  7736  caucvgsrlemoffres  7741  caucvgsr  7743  map2psrprg  7746  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  axprecex  7821  axpre-ltwlin  7824  axpre-lttrn  7825  axpre-apti  7826  axpre-ltadd  7827  axpre-mulgt0  7828  axpre-mulext  7829  axcaucvglemcau  7839  axcaucvglemres  7840  axcaucvg  7841  axpre-suploclemres  7842  axpre-suploc  7843  ltxrlt  7964  lttri3  7978  ltne  7983  eqle  7990  ltordlem  8380  reapti  8477  apreim  8501  squeeze0  8799  lbreu  8840  lble  8842  suprleubex  8849  sup3exmid  8852  nnge1  8880  nn2ge  8890  nn1gt1  8891  nnsub  8896  nominpos  9094  nn0ge0  9139  elnnnn0b  9158  nn0ge2m1nn  9174  zdclt  9268  suprzclex  9289  peano2uz2  9298  peano5uzti  9299  dfuzi  9301  uzind  9302  uzind3  9304  eluz1  9470  uzind4  9526  indstr  9531  supinfneg  9533  infsupneg  9534  infregelbex  9536  indstr2  9547  ublbneg  9551  elpq  9586  elpqb  9587  elrp  9591  mnfltxr  9722  nn0pnfge0  9727  xrltnsym  9729  xrlttr  9731  xrltso  9732  xrlttri3  9733  xrltne  9749  ngtmnft  9753  nmnfgt  9754  xrrebnd  9755  z2ge  9762  xltnegi  9771  xltadd1  9812  xsubge0  9817  xleaddadd  9823  ixxval  9832  elixx1  9833  elioo2  9857  iccid  9861  iccsupr  9902  repos  9906  fzval  9946  elfz1  9949  fzm1  10035  exbtwnzlemstep  10183  exbtwnzlemex  10185  qbtwnre  10192  qbtwnxr  10193  flval  10207  apbtwnz  10209  modqid2  10286  modqmuladdnn0  10303  exp3val  10457  expge0  10491  expge1  10492  nn0ltexp2  10623  facdiv  10651  facwordi  10653  hashinfom  10691  hashennn  10693  hashunlem  10717  zfz1iso  10754  ovshftex  10761  shftfibg  10762  shftfib  10765  shftfn  10766  2shfti  10773  sqrt0rlem  10945  resqrexlemex  10967  rsqrmo  10969  resqrtcl  10971  rersqrtthlem  10972  sqrtsq  10986  cau3lem  11056  caubnd2  11059  maxleim  11147  maxabslemval  11150  maxleast  11155  maxleb  11158  fimaxre2  11168  minmax  11171  xrmaxleim  11185  xrmaxiflemval  11191  xrmaxaddlem  11201  xrminmax  11206  xrbdtri  11217  climi  11228  climeu  11237  climmo  11239  2clim  11242  addcn2  11251  mulcn2  11253  reccn2ap  11254  cn1lem  11255  summodc  11324  zsumdc  11325  fsum3  11328  cvgratz  11473  ntrivcvgap0  11490  prodmodc  11519  zproddc  11520  fprodseq  11524  fprodntrivap  11525  dvdsabsb  11750  0dvds  11751  alzdvds  11792  dvdsext  11793  fzo0dvdseq  11795  2tp1odd  11821  2teven  11824  divalglemnn  11855  divalglemeunn  11858  divalglemeuneg  11860  zsupcllemstep  11878  suprzubdc  11885  zsupssdc  11887  gcdval  11892  gcddvds  11896  bezoutlemstep  11930  bezoutlemmain  11931  bezoutlemex  11934  bezoutlemeu  11940  bezoutlemsup  11942  dfgcd3  11943  bezout  11944  dvdsgcd  11945  dfgcd2  11947  dvdssq  11964  uzwodc  11970  nnwofdc  11971  lcmval  11995  lcmcllem  11999  dvdslcm  12001  lcmledvds  12002  lcmgcdlem  12009  lcmdvds  12011  coprmgcdb  12020  coprmdvds2  12025  cncongr1  12035  cncongr2  12036  isprm  12041  dvdsnprmd  12057  dvdsprm  12069  exprmfct  12070  isprm6  12079  prmexpb  12083  prmfac1  12084  rpexp  12085  sqrt2irr  12094  oddpwdclemdc  12105  oddpwdc  12106  sqpweven  12107  2sqpwodd  12108  sqne2sq  12109  nnoddn2prmb  12194  pceu  12227  pczpre  12229  pcdiv  12234  pcdvdsb  12251  difsqpwdvds  12269  pcmpt  12273  pcmptdvds  12275  oddprmdvds  12284  prmpwdvds  12285  infpnlem2  12290  oddennn  12325  evenennn  12326  exmidunben  12359  nninfdclemcl  12381  nninfdclemp1  12383  nninfdc  12386  infpn2  12389  comet  13139  metcnpi  13155  metcnpi2  13156  metcnpi3  13157  addcncntoplem  13191  cncfi  13205  elcncf1di  13206  mulcncflem  13230  dedekindeulemuub  13235  dedekindeulemloc  13237  dedekindeulemlu  13239  dedekindeulemeu  13240  dedekindeu  13241  suplociccreex  13242  suplociccex  13243  dedekindicclemuub  13244  dedekindicclemloc  13246  dedekindicclemlu  13248  dedekindicclemeu  13249  dedekindicclemicc  13250  dedekindicc  13251  ivthinclemlopn  13254  ivthinclemlr  13255  ivthinclemuopn  13256  ivthinclemur  13257  ivthinclemloc  13259  ivthinc  13261  limcimo  13274  cnplimclemr  13278  limccnp2lem  13285  limccoap  13287  eldvap  13291  logltb  13435  lgsdir  13576  lgsne0  13579  2sqlem6  13596  2sqlem8  13599  2sqlem10  13601  sbthom  13905  trilpo  13922  trirec0  13923  apdiff  13927  reap0  13937  nconstwlpolem  13943  neapmkv  13946