Theorem breq2d 3767

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

Hypothesis

Ref	Expression
breq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
breq2d	⊢ (φ → (𝐶𝑅A ↔ 𝐶𝑅B))

Proof of Theorem breq2d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (φ → A = B)
2		breq2 3759	. 2 ⊢ (A = B → (𝐶𝑅A ↔ 𝐶𝑅B))
3	1, 2	syl 14	1 ⊢ (φ → (𝐶𝑅A ↔ 𝐶𝑅B))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1242   class class class wbr 3755

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756

This theorem is referenced by:  breqtrd  3779  sbcbr1g  3806  pofun  4040  csbfv12g  5152  isorel  5391  isocnv  5394  isotr  5399  caovordig  5608  caovordg  5610  caovord  5614  xporderlem  5793  th3qlem2  6145  enqdc1  6346  ltanqg  6384  ltmnqg  6385  archnqq  6400  prarloclemarch2  6402  prloc  6473  addnqprllem  6509  addlocprlemgt  6516  appdivnq  6543  mulnqprl  6548  1idprl  6565  ltexprlemloc  6580  cauappcvgprlemcan  6615  cauappcvgprlemm  6616  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem1  6630  cauappcvgprlemlim  6632  cauappcvgpr  6633  ltposr  6671  ltasrg  6678  mulgt0sr  6684  mulextsr1lem  6686  mulextsr1  6687  pitonnlem2  6723  pitonn  6724  axpre-ltadd  6750  axpre-mulgt0  6751  axpre-mulext  6752  axarch  6753  ltsubadd2  7203  lesubadd2  7205  ltaddsub  7206  leaddsub  7208  ltaddpos2  7223  posdif  7225  lesub1  7226  ltsub1  7228  ltnegcon1  7233  lenegcon1  7236  addge02  7243  leaddle0  7247  apreap  7351  prodgt02  7580  prodge02  7582  ltmulgt12  7592  lemulge12  7594  ltdivmul  7603  ledivmul  7604  ltdivmul2  7605  lt2mul2div  7606  ledivmul2  7607  ltrec  7610  ltrec1  7615  ltdiv23  7619  lediv23  7620  nnge1  7698  halfpos  7913  lt2halves  7917  addltmul  7918  avglt2  7921  avgle2  7923  nnrecl  7935  zltlem1  8057  gtndiv  8091  qapne  8330  xltnegi  8498  divelunit  8620  eluzgtdifelfzo  8803  frec2uzltd  8850  frec2uzlt2d  8851  frec2uzf1od  8853  expnbnd  9005