Theorem breq2d 3776

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
breq2d	⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Proof of Theorem breq2d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq2 3768	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1243   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:  breqtrd  3788  sbcbr1g  3815  pofun  4049  csbfv12g  5209  isorel  5448  isocnv  5451  isotr  5456  caovordig  5666  caovordg  5668  caovord  5672  xporderlem  5852  th3qlem2  6209  phplem3g  6319  enqdc1  6460  ltanqg  6498  ltmnqg  6499  archnqq  6515  prarloclemarch2  6517  prloc  6589  addnqprllem  6625  addlocprlemgt  6632  appdivnq  6661  mulnqprl  6666  1idprl  6688  ltexprlemloc  6705  caucvgprlemcanl  6742  cauappcvgprlemm  6743  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  cauappcvgprlemlim  6759  cauappcvgpr  6760  archrecnq  6761  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemcl  6774  caucvgprlemladdrl  6776  caucvgpr  6780  caucvgprprlemell  6783  caucvgprprlemelu  6784  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemnkeqj  6788  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlemclphr  6803  caucvgprprlemexbt  6804  caucvgprprlem1  6807  caucvgprprlem2  6808  caucvgprpr  6810  ltposr  6848  ltasrg  6855  mulgt0sr  6862  mulextsr1lem  6864  mulextsr1  6865  prsrlt  6871  caucvgsrlemcl  6873  caucvgsrlemfv  6875  caucvgsrlembound  6878  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  caucvgsr  6886  pitonnlem2  6923  pitonn  6924  recidpipr  6932  axpre-ltadd  6960  axpre-mulgt0  6961  axpre-mulext  6962  axarch  6965  nntopi  6968  axcaucvglemval  6971  axcaucvglemcau  6972  axcaucvglemres  6973  ltsubadd2  7428  lesubadd2  7430  ltaddsub  7431  leaddsub  7433  ltaddpos2  7448  posdif  7450  lesub1  7451  ltsub1  7453  ltnegcon1  7458  lenegcon1  7461  addge02  7468  leaddle0  7472  possumd  7560  sublt0d  7561  apreap  7578  prodgt02  7819  prodge02  7821  ltmulgt12  7831  lemulge12  7833  ltdivmul  7842  ledivmul  7843  ltdivmul2  7844  lt2mul2div  7845  ledivmul2  7846  ltrec  7849  ltrec1  7854  ltdiv23  7858  lediv23  7859  nnge1  7937  halfpos  8156  lt2halves  8160  addltmul  8161  avglt2  8164  avgle2  8166  nnrecl  8179  zltlem1  8301  gtndiv  8335  qapne  8574  xltnegi  8748  divelunit  8870  eluzgtdifelfzo  9053  qtri3or  9098  qbtwnzlemstep  9103  qbtwnzlemshrink  9104  qbtwnzlemex  9105  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2zlemshrink  9108  rebtwn2z  9109  flqlelt  9118  flqbi  9132  2tnp1ge0ge0  9143  frec2uzltd  9189  frec2uzlt2d  9190  frec2uzf1od  9192  monoord  9235  isermono  9237  expnbnd  9372  caucvgrelemcau  9579  caucvgre  9580  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniq  9593  resqrexlemover  9608  resqrexlemgt0  9618  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemsqa  9622  resqrexlemex  9623  climserile  9865  nn0seqcvgd  9880