Theorem breq2 4049

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ wcel 2176  ⟨cop 3636   class class class wbr 4045

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046

This theorem is referenced by:  breq12  4050  breq2i  4053  breq2d  4057  nbrne1  4064  brralrspcev  4103  brimralrspcev  4104  pocl  4351  swopolem  4353  swopo  4354  sowlin  4368  sotricim  4371  sotritrieq  4373  seex  4383  frind  4400  wetriext  4626  vtoclr  4724  posng  4748  brcog  4846  brcogw  4848  opelcnvg  4859  dfdmf  4872  breldmg  4885  dfrnf  4920  dmcoss  4949  resieq  4970  dfres2  5012  elimag  5027  elrelimasn  5049  elimasn  5050  intirr  5070  poirr2  5076  poltletr  5084  dffun6f  5285  dffun4f  5288  fun11  5342  brprcneu  5571  fv3  5601  tz6.12c  5608  relelfvdm  5610  funbrfv  5619  fnbrfvb  5621  funfvdm2f  5646  fndmdif  5687  dff3im  5727  fmptco  5748  foeqcnvco  5861  isorel  5879  isocnv  5882  isotr  5887  isopolem  5893  isosolem  5895  f1oiso  5897  f1oiso2  5898  caovordig  6114  caovordg  6116  caovord  6120  caofrss  6192  caoftrn  6193  poxp  6320  tposoprab  6368  ertr  6637  ecopovsym  6720  ecopovtrn  6721  ecopovsymg  6723  ecopovtrng  6724  th3qlem2  6727  domeng  6843  eqeng  6859  snfig  6908  nneneq  6956  nnfi  6971  ssfilem  6974  domfiexmid  6977  dif1enen  6979  diffitest  6986  findcard  6987  findcard2  6988  findcard2s  6989  diffisn  6992  tridc  6998  fimax2gtrilemstep  6999  inffiexmid  7005  unsnfi  7018  fiintim  7030  fisseneq  7033  isbth  7071  supmoti  7097  eqsupti  7100  supubti  7103  suplubti  7104  suplub2ti  7105  supmaxti  7108  supsnti  7109  isotilem  7110  isoti  7111  supisolem  7112  supisoex  7113  cardcl  7290  isnumi  7291  cardval3ex  7294  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  exmidapne  7374  nqtri3or  7511  ltsonq  7513  ltanqg  7515  ltmnqg  7516  ltexnqq  7523  nsmallnqq  7527  subhalfnqq  7529  ltbtwnnqq  7530  prarloclemarch2  7534  nqnq0pi  7553  prcdnql  7599  prcunqu  7600  prnminu  7604  genpcdl  7634  genprndl  7636  genprndu  7637  genpdisj  7638  nqprm  7657  nqprrnd  7658  nqprdisj  7659  nqprloc  7660  nqprlu  7662  nqprl  7666  addnqprlemru  7673  addnqprlemfl  7674  addnqprlemfu  7675  mulnqprlemru  7689  mulnqprlemfl  7690  mulnqprlemfu  7691  1idpru  7706  ltnqpr  7708  ltnqpri  7709  prplnqu  7735  recexprlemelu  7738  recexprlemm  7739  recexprlemloc  7746  recexprlem1ssl  7748  recexprlemss1u  7751  cauappcvgprlemm  7760  cauappcvgprlemopu  7763  cauappcvgprlemupu  7764  cauappcvgprlemdisj  7766  cauappcvgprlemloc  7767  cauappcvgprlemladdfu  7769  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem2  7775  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemm  7783  caucvgprlemopu  7786  caucvgprlemupu  7787  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemcl  7791  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  caucvgprlem2  7795  caucvgprprlemelu  7801  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemnbj  7808  caucvgprprlemmu  7810  caucvgprprlemexbt  7821  caucvgprprlemaddq  7823  caucvgprprlem1  7824  caucvgprprlem2  7825  suplocexprlemmu  7833  suplocexprlemru  7834  suplocexprlemdisj  7835  suplocexprlemloc  7836  suplocexprlemub  7838  suplocexpr  7840  lttrsr  7877  ltsosr  7879  ltasrg  7885  recexgt0sr  7888  mulgt0sr  7893  aptisr  7894  mulextsr1  7896  srpospr  7898  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  caucvgsr  7917  map2psrprg  7920  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  axprecex  7995  axpre-ltwlin  7998  axpre-lttrn  7999  axpre-apti  8000  axpre-ltadd  8001  axpre-mulgt0  8002  axpre-mulext  8003  axcaucvglemcau  8013  axcaucvglemres  8014  axcaucvg  8015  axpre-suploclemres  8016  axpre-suploc  8017  ltxrlt  8140  lttri3  8154  ltne  8159  eqle  8166  ltordlem  8557  reapti  8654  apreim  8678  squeeze0  8979  lbreu  9020  lble  9022  suprleubex  9029  sup3exmid  9032  nnge1  9061  nn2ge  9071  nn1gt1  9072  nnsub  9077  nominpos  9277  nn0ge0  9322  elnnnn0b  9341  nn0ge2m1nn  9357  zdclt  9452  suprzclex  9473  peano2uz2  9482  peano5uzti  9483  dfuzi  9485  uzind  9486  uzind3  9488  eluz1  9654  uzind4  9711  indstr  9716  supinfneg  9718  infsupneg  9719  infregelbex  9721  indstr2  9732  ublbneg  9736  irrmulap  9771  elpq  9772  elpqb  9773  elrp  9779  mnfltxr  9910  nn0pnfge0  9915  xrltnsym  9917  xrlttr  9919  xrltso  9920  xrlttri3  9921  xrltne  9937  ngtmnft  9941  nmnfgt  9942  xrrebnd  9943  z2ge  9950  xltnegi  9959  xltadd1  10000  xsubge0  10005  xleaddadd  10011  ixxval  10020  elixx1  10021  elioo2  10045  iccid  10049  iccsupr  10090  repos  10094  fzval  10134  elfz1  10137  fzm1  10224  zsupcllemstep  10374  suprzubdc  10381  zsupssdc  10383  qdclt  10390  exbtwnzlemstep  10392  exbtwnzlemex  10394  qbtwnre  10401  qbtwnxr  10402  flval  10417  apbtwnz  10419  modqid2  10498  modqmuladdnn0  10515  exp3val  10688  expge0  10722  expge1  10723  nn0ltexp2  10856  facdiv  10885  facwordi  10887  hashinfom  10925  hashennn  10927  hashunlem  10951  zfz1iso  10988  wrdlen1  11033  fstwrdne0  11035  wrdl1exs1  11086  pfxsuffeqwrdeq  11152  pfxsuff1eqwrdeq  11153  ovshftex  11163  shftfibg  11164  shftfib  11167  shftfn  11168  2shfti  11175  sqrt0rlem  11347  resqrexlemex  11369  rsqrmo  11371  resqrtcl  11373  rersqrtthlem  11374  sqrtsq  11388  cau3lem  11458  caubnd2  11461  maxleim  11549  maxabslemval  11552  maxleast  11557  maxleb  11560  fimaxre2  11571  minmax  11574  xrmaxleim  11588  xrmaxiflemval  11594  xrmaxaddlem  11604  xrminmax  11609  xrbdtri  11620  climi  11631  climeu  11640  climmo  11642  2clim  11645  addcn2  11654  mulcn2  11656  reccn2ap  11657  cn1lem  11658  summodc  11727  zsumdc  11728  fsum3  11731  cvgratz  11876  ntrivcvgap0  11893  prodmodc  11922  zproddc  11923  fprodseq  11927  fprodntrivap  11928  sinltxirr  12105  dvdsabsb  12154  0dvds  12155  alzdvds  12198  dvdsext  12199  fzo0dvdseq  12201  2tp1odd  12228  2teven  12231  divalglemnn  12262  divalglemeunn  12265  divalglemeuneg  12267  bitsinv1lem  12305  gcdval  12313  gcddvds  12317  bezoutlemstep  12351  bezoutlemmain  12352  bezoutlemex  12355  bezoutlemeu  12361  bezoutlemsup  12363  dfgcd3  12364  bezout  12365  dvdsgcd  12366  dfgcd2  12368  dvdssq  12385  uzwodc  12391  nnwofdc  12392  lcmval  12418  lcmcllem  12422  dvdslcm  12424  lcmledvds  12425  lcmgcdlem  12432  lcmdvds  12434  coprmgcdb  12443  coprmdvds2  12448  cncongr1  12458  cncongr2  12459  isprm  12464  dvdsnprmd  12480  dvdsprm  12492  exprmfct  12493  isprm6  12502  prmexpb  12506  prmfac1  12507  rpexp  12508  sqrt2irr  12517  oddpwdclemdc  12528  oddpwdc  12529  sqpweven  12530  2sqpwodd  12531  sqne2sq  12532  nnoddn2prmb  12618  pceu  12651  pczpre  12653  pcdiv  12658  pcdvdsb  12676  difsqpwdvds  12694  pcmpt  12699  pcmptdvds  12701  oddprmdvds  12710  prmpwdvds  12711  infpnlem2  12716  oddennn  12796  evenennn  12797  exmidunben  12830  nninfdclemcl  12852  nninfdclemp1  12854  nninfdc  12857  infpn2  12860  eqgen  13596  zndvds  14444  znleval  14448  comet  15004  metcnpi  15020  metcnpi2  15021  metcnpi3  15022  addcncntoplem  15066  cncfi  15083  elcncf1di  15084  mulcncflem  15112  dedekindeulemuub  15122  dedekindeulemloc  15124  dedekindeulemlu  15126  dedekindeulemeu  15127  dedekindeu  15128  suplociccreex  15129  suplociccex  15130  dedekindicclemuub  15131  dedekindicclemloc  15133  dedekindicclemlu  15135  dedekindicclemeu  15136  dedekindicclemicc  15137  dedekindicc  15138  ivthinclemlopn  15141  ivthinclemlr  15142  ivthinclemuopn  15143  ivthinclemur  15144  ivthinclemloc  15146  ivthinc  15148  ivthreinc  15150  dich0  15157  ivthdich  15158  limcimo  15170  cnplimclemr  15174  limccnp2lem  15181  limccoap  15183  eldvap  15187  logltb  15379  lgsdir  15545  lgsne0  15548  gausslemma2dlem0i  15567  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  2lgslem2  15602  2lgs  15614  2sqlem6  15630  2sqlem8  15633  2sqlem10  15635  sbthom  16002  trilpo  16019  trirec0  16020  apdiff  16024  reap0  16034  cndcap  16035  nconstwlpolem  16041  neapmkv  16044  neap0mkv  16045  ltlenmkv  16046