Theorem breq2 3768

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

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1243   ∈ wcel 1393  ⟨cop 3378   class class class wbr 3764

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-br 3765

This theorem is referenced by:  breq12  3769  breq2i  3772  breq2d  3776  nbrne1  3781  pocl  4040  swopolem  4042  swopo  4043  sowlin  4057  sotricim  4060  sotritrieq  4062  seex  4072  frind  4089  wetriext  4301  vtoclr  4388  posng  4412  brcog  4502  brcogw  4504  opelcnvg  4515  dfdmf  4528  breldmg  4541  dfrnf  4575  dmcoss  4601  resieq  4622  dfres2  4658  elimag  4672  elreimasng  4691  elimasn  4692  intirr  4711  poirr2  4717  poltletr  4725  dffun6f  4915  dffun4f  4918  fun11  4966  brprcneu  5171  fv3  5197  tz6.12c  5203  relelfvdm  5205  funbrfv  5212  fnbrfvb  5214  funfvdm2f  5238  fndmdif  5272  dff3im  5312  fmptco  5330  foeqcnvco  5430  isorel  5448  isocnv  5451  isotr  5456  isopolem  5461  isosolem  5463  f1oiso  5465  f1oiso2  5466  caovordig  5666  caovordg  5668  caovord  5672  caofrss  5735  caoftrn  5736  poxp  5853  tposoprab  5895  ertr  6121  ecopovsym  6202  ecopovtrn  6203  ecopovsymg  6205  ecopovtrng  6206  th3qlem2  6209  domeng  6233  eqeng  6246  snfig  6291  nneneq  6320  nnfi  6333  ssfiexmid  6336  diffitest  6344  findcard  6345  findcard2  6346  findcard2s  6347  diffisn  6350  cardcl  6361  isnumi  6362  cardval3ex  6365  nqtri3or  6494  ltsonq  6496  ltanqg  6498  ltmnqg  6499  ltexnqq  6506  nsmallnqq  6510  subhalfnqq  6512  ltbtwnnqq  6513  prarloclemarch2  6517  nqnq0pi  6536  prcdnql  6582  prcunqu  6583  prnminu  6587  genpcdl  6617  genprndl  6619  genprndu  6620  genpdisj  6621  nqprm  6640  nqprrnd  6641  nqprdisj  6642  nqprloc  6643  nqprlu  6645  nqprl  6649  addnqprlemru  6656  addnqprlemfl  6657  addnqprlemfu  6658  mulnqprlemru  6672  mulnqprlemfl  6673  mulnqprlemfu  6674  1idpru  6689  ltnqpr  6691  ltnqpri  6692  prplnqu  6718  recexprlemelu  6721  recexprlemm  6722  recexprlemloc  6729  recexprlem1ssl  6731  recexprlemss1u  6734  cauappcvgprlemm  6743  cauappcvgprlemopu  6746  cauappcvgprlemupu  6747  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem2  6758  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemopu  6769  caucvgprlemupu  6770  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemcl  6774  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem2  6778  caucvgprprlemelu  6784  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemnbj  6791  caucvgprprlemmu  6793  caucvgprprlemexbt  6804  caucvgprprlemaddq  6806  caucvgprprlem1  6807  caucvgprprlem2  6808  lttrsr  6847  ltsosr  6849  ltasrg  6855  recexgt0sr  6858  mulgt0sr  6862  aptisr  6863  mulextsr1  6865  srpospr  6867  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  caucvgsr  6886  axprecex  6954  axpre-ltwlin  6957  axpre-lttrn  6958  axpre-apti  6959  axpre-ltadd  6960  axpre-mulgt0  6961  axpre-mulext  6962  axcaucvglemcau  6972  axcaucvglemres  6973  axcaucvg  6974  ltxrlt  7085  lttri3  7098  ltne  7103  eqle  7109  reapti  7570  apreim  7594  squeeze0  7870  nnge1  7937  nn2ge  7946  nn1gt1  7947  nnsub  7952  nominpos  8162  nn0ge0  8207  elnnnn0b  8226  nn0ge2m1nn  8242  zdclt  8318  peano2uz2  8345  peano5uzti  8346  dfuzi  8348  uzind  8349  uzind3  8351  eluz1  8477  uzind4  8531  indstr  8536  indstr2  8546  ublbneg  8548  elrp  8585  mnfltxr  8707  nn0pnfge0  8712  xrltnsym  8714  xrlttr  8716  xrltso  8717  xrlttri3  8718  xrltne  8729  ngtmnft  8731  xrrebnd  8732  z2ge  8739  xltnegi  8748  ixxval  8765  elixx1  8766  elioo2  8790  iccid  8794  iccsupr  8835  repos  8839  fzval  8876  elfz1  8879  fzm1  8962  qbtwnre  9111  flval  9116  serige0  9252  expival  9257  expge0  9291  expge1  9292  ovshftex  9420  shftfibg  9421  shftfib  9424  shftfn  9425  2shfti  9432  sqrt0rlem  9601  resqrexlemex  9623  rsqrmo  9625  resqrtcl  9627  rersqrtthlem  9628  sqrtsq  9642  cau3lem  9710  caubnd2  9713  climi  9808  climeu  9817  climmo  9819  2clim  9822  addcn2  9831  mulcn2  9833  cn1lem  9834  sqrt2irr  9878