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-bndl 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  6474  addnqprllem  6510  addlocprlemgt  6517  appdivnq  6544  mulnqprl  6549  1idprl  6566  ltexprlemloc  6581  cauappcvgprlemcan  6616  cauappcvgprlemm  6617  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  cauappcvgprlemlim  6633  cauappcvgpr  6634  archrecnq  6635  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemm  6639  caucvgprlemcl  6647  caucvgprlemladdrl  6649  caucvgpr  6653  ltposr  6691  ltasrg  6698  mulgt0sr  6704  mulextsr1lem  6706  mulextsr1  6707  pitonnlem2  6743  pitonn  6744  axpre-ltadd  6770  axpre-mulgt0  6771  axpre-mulext  6772  axarch  6773  ltsubadd2  7223  lesubadd2  7225  ltaddsub  7226  leaddsub  7228  ltaddpos2  7243  posdif  7245  lesub1  7246  ltsub1  7248  ltnegcon1  7253  lenegcon1  7256  addge02  7263  leaddle0  7267  apreap  7371  prodgt02  7600  prodge02  7602  ltmulgt12  7612  lemulge12  7614  ltdivmul  7623  ledivmul  7624  ltdivmul2  7625  lt2mul2div  7626  ledivmul2  7627  ltrec  7630  ltrec1  7635  ltdiv23  7639  lediv23  7640  nnge1  7718  halfpos  7933  lt2halves  7937  addltmul  7938  avglt2  7941  avgle2  7943  nnrecl  7955  zltlem1  8077  gtndiv  8111  qapne  8350  xltnegi  8518  divelunit  8640  eluzgtdifelfzo  8823  frec2uzltd  8870  frec2uzlt2d  8871  frec2uzf1od  8873  expnbnd  9025