Theorem breq2d 3887

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 3879	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1299   class class class wbr 3875

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483  df-br 3876

This theorem is referenced by:  breqtrd  3899  sbcbr1g  3926  pofun  4172  csbfv12g  5389  isorel  5641  isocnv  5644  isotr  5649  caovordig  5868  caovordg  5870  caovord  5874  xporderlem  6058  th3qlem2  6462  phplem3g  6679  supsnti  6807  inflbti  6826  difinfinf  6901  enqdc1  7071  ltanqg  7109  ltmnqg  7110  archnqq  7126  prarloclemarch2  7128  prloc  7200  addnqprllem  7236  addlocprlemgt  7243  appdivnq  7272  mulnqprl  7277  1idprl  7299  ltexprlemloc  7316  caucvgprlemcanl  7353  cauappcvgprlemm  7354  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  cauappcvgprlem1  7368  cauappcvgprlemlim  7370  cauappcvgpr  7371  archrecnq  7372  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemm  7377  caucvgprlemcl  7385  caucvgprlemladdrl  7387  caucvgpr  7391  caucvgprprlemell  7394  caucvgprprlemelu  7395  caucvgprprlemcbv  7396  caucvgprprlemval  7397  caucvgprprlemnkeqj  7399  caucvgprprlemml  7403  caucvgprprlemmu  7404  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemopu  7408  caucvgprprlemloc  7412  caucvgprprlemclphr  7414  caucvgprprlemexbt  7415  caucvgprprlem1  7418  caucvgprprlem2  7419  caucvgprpr  7421  ltposr  7459  ltasrg  7466  mulgt0sr  7473  mulextsr1lem  7475  mulextsr1  7476  prsrlt  7482  caucvgsrlemcl  7484  caucvgsrlemfv  7486  caucvgsrlembound  7489  caucvgsrlemgt1  7490  caucvgsrlemoffres  7495  caucvgsr  7497  pitonnlem2  7534  pitonn  7535  recidpipr  7543  axpre-ltadd  7571  axpre-mulgt0  7572  axpre-mulext  7573  axarch  7576  nntopi  7579  axcaucvglemval  7582  axcaucvglemcau  7583  axcaucvglemres  7584  ltaddneg  8053  ltsubadd2  8062  lesubadd2  8064  ltaddsub  8065  leaddsub  8067  ltaddpos2  8082  posdif  8084  lesub1  8085  ltsub1  8087  ltnegcon1  8092  lenegcon1  8095  addge02  8102  leaddle0  8106  ltordlem  8111  possumd  8197  sublt0d  8198  apreap  8215  prodgt02  8469  prodge02  8471  ltmulgt12  8481  lemulge12  8483  ltdivmul  8492  ledivmul  8493  ltdivmul2  8494  lt2mul2div  8495  ledivmul2  8496  ltrec  8499  ltrec1  8504  ltdiv23  8508  lediv23  8509  nnge1  8601  halfpos  8803  lt2halves  8807  addltmul  8808  avglt2  8811  avgle2  8813  nnrecl  8827  zltlem1  8963  nn0le2is012  8985  gtndiv  8998  qapne  9281  nnledivrp  9394  xltnegi  9459  xltadd1  9500  xsubge0  9505  xposdif  9506  xlesubadd  9507  xleaddadd  9511  divelunit  9626  eluzgtdifelfzo  9815  qtri3or  9861  exbtwnzlemstep  9866  exbtwnzlemshrink  9867  exbtwnzlemex  9868  exbtwnz  9869  rebtwn2zlemstep  9871  rebtwn2zlemshrink  9872  rebtwn2z  9873  flqlelt  9890  flqbi  9904  2tnp1ge0ge0  9915  q2submod  9999  frec2uzltd  10017  frec2uzlt2d  10018  frec2uzf1od  10020  monoord  10090  ser3mono  10092  ser3ge0  10131  expnbnd  10256  facwordi  10327  hashunlem  10391  zfz1isolemiso  10423  seq3coll  10426  caucvgrelemcau  10592  caucvgre  10593  cvg1nlemcau  10596  cvg1nlemres  10597  recvguniq  10607  resqrexlemover  10622  resqrexlemgt0  10632  resqrexlemoverl  10633  resqrexlemglsq  10634  resqrexlemsqa  10636  resqrexlemex  10637  maxleastlt  10827  minmax  10840  lemininf  10844  ltmininf  10845  xrmaxleastlt  10864  xrmaxltsup  10866  xrminmax  10873  xrmin1inf  10875  xrmin2inf  10876  xrltmininf  10878  xrlemininf  10879  climserle  10953  summodclem3  10988  summodclem2a  10989  summodc  10991  zsumdc  10992  fsum3  10995  fsum00  11070  fsumabs  11073  cvgratnnlemnexp  11132  cvgratnnlemmn  11133  sin01bnd  11262  cos01bnd  11263  summodnegmod  11319  modmulconst  11320  dvdsaddr  11332  dvdssub  11333  dvdssubr  11334  dvdslelemd  11336  dvdsfac  11353  dvdsmod  11355  oddp1even  11368  ltoddhalfle  11385  opoe  11387  omoe  11388  divalg2  11418  divalgmod  11419  ndvdssub  11422  ndvdsadd  11423  bezoutlembi  11486  dvdssqim  11505  dvdsmulgcd  11506  dvdssq  11512  nn0seqcvgd  11515  coprmdvds  11566  coprmdvds2  11567  rpmul  11572  cncongr1  11577  divgcdodd  11614  isprm6  11618  prmdvdsexp  11619  prmdvdsexpr  11621  prmfac1  11623  oddpwdclemxy  11639  oddpwdclemodd  11642  sqpweven  11645  2sqpwodd  11646  sqne2sq  11647  hashdvds  11689  phiprmpw  11690  exmidunben  11731  psmettri2  12256  ismet2  12282  xmettri2  12289  comet  12427  limccl  12510  ellimc3ap  12511