Theorem breq2 4129

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ⟨cop 3708   class class class wbr 4125

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-br 4126

This theorem is referenced by:  breq12  4130  breq2i  4133  breq2d  4137  nbrne1  4144  brralrspcev  4184  brimralrspcev  4185  pocl  4443  swopolem  4445  swopo  4446  sowlin  4460  sotricim  4463  sotritrieq  4465  seex  4475  frind  4492  wetriext  4719  vtoclr  4818  posng  4842  brcog  4942  brcogw  4944  opelcnvg  4955  dfdmf  4969  breldmg  4982  dfrnf  5018  dmcoss  5047  resieq  5068  dfres2  5110  elimag  5125  elrelimasn  5148  elimasn  5149  intirr  5169  poirr2  5175  poltletr  5183  dffun6f  5385  dffun4f  5388  fun11  5443  brprcneu  5683  fv3  5713  tz6.12c  5720  relelfvdm  5722  fvmbr  5725  funbrfv  5733  fnbrfvb  5735  funfvdm2f  5762  fndmdif  5805  dff3im  5844  fmptco  5865  foeqcnvco  5986  isorel  6004  isocnv  6007  isotr  6012  isopolem  6018  isosolem  6020  f1oiso  6022  f1oiso2  6023  caovordig  6245  caovordg  6247  caovord  6251  caofrss  6324  caoftrn  6325  poxp  6458  tposoprab  6541  ertr  6812  ecopovsym  6895  ecopovtrn  6896  ecopovsymg  6898  ecopovtrng  6899  th3qlem2  6902  domeng  7026  eqeng  7042  snfig  7093  nneneq  7148  nnfi  7164  ssfilem  7167  ssfilemd  7169  domfiexmid  7172  dif1enen  7174  diffitest  7181  findcard  7182  findcard2  7183  findcard2s  7184  diffisn  7187  tridc  7194  fimax2gtrilemstep  7195  inffiexmid  7203  unsnfi  7216  fiintim  7228  fisseneq  7232  isbth  7274  supmoti  7323  eqsupti  7326  supubti  7329  suplubti  7330  suplub2ti  7331  supmaxti  7334  supsnti  7335  isotilem  7336  isoti  7337  supisolem  7338  supisoex  7339  cardcl  7516  isnumi  7517  cardval3ex  7520  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  papsym  7602  papcotr  7603  exmidapne  7616  nqtri3or  7753  ltsonq  7755  ltanqg  7757  ltmnqg  7758  ltexnqq  7765  nsmallnqq  7769  subhalfnqq  7771  ltbtwnnqq  7772  prarloclemarch2  7776  nqnq0pi  7795  prcdnql  7841  prcunqu  7842  prnminu  7846  genpcdl  7876  genprndl  7878  genprndu  7879  genpdisj  7880  nqprm  7899  nqprrnd  7900  nqprdisj  7901  nqprloc  7902  nqprlu  7904  nqprl  7908  addnqprlemru  7915  addnqprlemfl  7916  addnqprlemfu  7917  mulnqprlemru  7931  mulnqprlemfl  7932  mulnqprlemfu  7933  1idpru  7948  ltnqpr  7950  ltnqpri  7951  prplnqu  7977  recexprlemelu  7980  recexprlemm  7981  recexprlemloc  7988  recexprlem1ssl  7990  recexprlemss1u  7993  cauappcvgprlemm  8002  cauappcvgprlemopu  8005  cauappcvgprlemupu  8006  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdfu  8011  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem2  8017  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemm  8025  caucvgprlemopu  8028  caucvgprlemupu  8029  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemcl  8033  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprlem2  8037  caucvgprprlemelu  8043  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemnbj  8050  caucvgprprlemmu  8052  caucvgprprlemexbt  8063  caucvgprprlemaddq  8065  caucvgprprlem1  8066  caucvgprprlem2  8067  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemub  8080  suplocexpr  8082  lttrsr  8119  ltsosr  8121  ltasrg  8127  recexgt0sr  8130  mulgt0sr  8135  aptisr  8136  mulextsr1  8138  srpospr  8140  caucvgsrlemgt1  8152  caucvgsrlemoffres  8157  caucvgsr  8159  map2psrprg  8162  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  axprecex  8237  axpre-ltwlin  8240  axpre-lttrn  8241  axpre-apti  8242  axpre-ltadd  8243  axpre-mulgt0  8244  axpre-mulext  8245  axcaucvglemcau  8255  axcaucvglemres  8256  axcaucvg  8257  axpre-suploclemres  8258  axpre-suploc  8259  ltxrlt  8381  lttri3  8395  ltne  8400  eqle  8407  ltordlem  8800  reapti  8897  apreim  8921  squeeze0  9224  lbreu  9265  lble  9267  suprleubex  9274  sup3exmid  9277  nnge1  9306  nn2ge  9316  nn1gt1  9317  nnsub  9322  nominpos  9522  nn0ge0  9567  elnnnn0b  9586  nn0ge2m1nn  9606  zdclt  9701  suprzclex  9723  peano2uz2  9732  peano5uzti  9733  dfuzi  9735  uzind  9736  uzind3  9738  eluz1  9904  uzind4  9967  indstr  9972  supinfneg  9974  infsupneg  9975  infregelbex  9977  indstr2  9988  ublbneg  9992  irrmulap  10027  elpq  10028  elpqb  10029  elrp  10035  mnfltxr  10167  nn0pnfge0  10172  xrltnsym  10174  xrlttr  10176  xrltso  10177  xrlttri3  10178  xrltne  10194  ngtmnft  10198  nmnfgt  10199  xrrebnd  10200  z2ge  10207  xltnegi  10216  xltadd1  10257  xsubge0  10262  xleaddadd  10268  ixxval  10277  elixx1  10278  elioo2  10302  iccid  10306  iccsupr  10347  repos  10351  fzval  10392  elfz1  10395  fzm1  10485  zsupcllemstep  10640  suprzubdc  10649  zsupssdc  10651  qdclt  10658  exbtwnzlemstep  10660  exbtwnzlemex  10662  qbtwnre  10669  qbtwnxr  10670  flval  10685  apbtwnz  10687  modqid2  10766  modqmuladdnn0  10783  exp3val  10956  expge0  10990  expge1  10991  nn0ltexp2  11125  facdiv  11154  facwordi  11156  hashinfom  11195  hashennn  11197  hashunlem  11222  zfz1iso  11271  wrdlen1  11320  fstwrdne0  11322  wrdl1exs1  11375  pfxsuffeqwrdeq  11448  pfxsuff1eqwrdeq  11449  ccats1pfxeq  11464  ccats1pfxeqrex  11465  pfxccatin12lem3  11482  ovshftex  11562  shftfibg  11563  shftfib  11566  shftfn  11567  2shfti  11574  sqrt0rlem  11747  resqrexlemex  11769  rsqrmo  11771  resqrtcl  11773  rersqrtthlem  11774  sqrtsq  11788  cau3lem  11858  caubnd2  11861  maxleim  11949  maxabslemval  11952  maxleast  11957  maxleb  11960  fimaxre2  11971  minmax  11974  xrmaxleim  11988  xrmaxiflemval  11994  xrmaxaddlem  12004  xrminmax  12009  xrbdtri  12020  climi  12031  climeu  12040  climmo  12042  2clim  12045  addcn2  12054  mulcn2  12056  reccn2ap  12057  cn1lem  12058  summodc  12128  zsumdc  12129  fsum3  12132  cvgratz  12277  ntrivcvgap0  12294  prodmodc  12323  zproddc  12324  fprodseq  12328  fprodntrivap  12329  sinltxirr  12506  dvdsabsb  12555  0dvds  12556  alzdvds  12599  dvdsext  12600  fzo0dvdseq  12602  2tp1odd  12629  2teven  12632  divalglemnn  12663  divalglemeunn  12666  divalglemeuneg  12668  bitsinv1lem  12706  gcdval  12714  gcddvds  12718  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlemex  12756  bezoutlemeu  12762  bezoutlemsup  12764  dfgcd3  12765  bezout  12766  dvdsgcd  12767  dfgcd2  12769  dvdssq  12786  uzwodc  12792  nnwofdc  12793  lcmval  12819  lcmcllem  12823  dvdslcm  12825  lcmledvds  12826  lcmgcdlem  12833  lcmdvds  12835  coprmgcdb  12844  coprmdvds2  12849  cncongr1  12859  cncongr2  12860  isprm  12865  dvdsnprmd  12881  dvdsprm  12893  exprmfct  12894  isprm6  12903  prmexpb  12907  prmfac1  12908  rpexp  12909  sqrt2irr  12918  oddpwdclemdc  12929  oddpwdc  12930  sqpweven  12931  2sqpwodd  12932  sqne2sq  12933  nnoddn2prmb  13019  pceu  13052  pczpre  13054  pcdiv  13059  pcdvdsb  13077  difsqpwdvds  13095  pcmpt  13100  pcmptdvds  13102  oddprmdvds  13111  prmpwdvds  13112  infpnlem2  13117  ballotfilemfcc  13211  oddennn  13261  evenennn  13262  exmidunben  13295  nninfdclemcl  13317  nninfdclemp1  13319  nninfdc  13322  infpn2  13325  eqgen  14007  zndvds  14956  znleval  14960  comet  15523  metcnpi  15539  metcnpi2  15540  metcnpi3  15541  addcncntoplem  15585  cncfi  15602  elcncf1di  15603  mulcncflem  15631  dedekindeulemuub  15641  dedekindeulemloc  15643  dedekindeulemlu  15645  dedekindeulemeu  15646  dedekindeu  15647  suplociccreex  15648  suplociccex  15649  dedekindicclemuub  15650  dedekindicclemloc  15652  dedekindicclemlu  15654  dedekindicclemeu  15655  dedekindicclemicc  15656  dedekindicc  15657  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemloc  15665  ivthinc  15667  ivthreinc  15669  dich0  15676  ivthdich  15677  limcimo  15689  cnplimclemr  15693  limccnp2lem  15700  limccoap  15702  eldvap  15706  logltb  15898  pellexlem3  16007  lgsdir  16068  lgsne0  16071  gausslemma2dlem0i  16090  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  2lgslem2  16125  2lgs  16137  2sqlem6  16153  2sqlem8  16156  2sqlem10  16158  lfgredg2dom  16287  istrl  16540  clwwlkn0  16563  clwwlkext2edg  16577  clwwlknonccat  16588  clwwlknonex2  16594  iseupth  16602  konigsberg  16648  lealltlt2  16666  sbthom  16976  trilpo  16997  trirec0  16998  apdiff  17002  reap0  17013  cndcap  17014  nconstwlpolem  17020  neapmkv  17023  neap0mkv  17024  ltlenmkv  17025