Theorem breq2d 3739

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 3731	. 2 ⊢ (A = B → (𝐶𝑅A ↔ 𝐶𝑅B))
3	1, 2	syl 14	1 ⊢ (φ → (𝐶𝑅A ↔ 𝐶𝑅B))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1223   class class class wbr 3727

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 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995

This theorem depends on definitions:  df-bi 110  df-3an 869  df-tru 1226  df-nf 1323  df-sb 1619  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-v 2528  df-un 2890  df-sn 3345  df-pr 3346  df-op 3348  df-br 3728

This theorem is referenced by:  breqtrd  3751  sbcbr1g  3778  pofun  4012  csbfv12g  5122  isorel  5361  isocnv  5364  isotr  5369  caovordig  5577  caovordg  5579  caovord  5583  xporderlem  5762  th3qlem2  6108  enqdc1  6207  ltanqg  6245  ltmnqg  6246  archnqq  6260  prarloclemarch2  6262  prloc  6331  addnqprllem  6368  addlocprlemgt  6375  appdivnq  6393  mulnqprl  6398  1idprl  6415  ltexprlemloc  6430  ltposr  6501  ltasrg  6508  mulgt0sr  6514  mulextsr1lem  6516  mulextsr1  6517  axpre-ltadd  6575  axpre-mulgt0  6576  axpre-mulext  6577  ltsubadd2  7026  lesubadd2  7028  ltaddsub  7029  leaddsub  7031  ltaddpos2  7046  posdif  7048  lesub1  7049  ltsub1  7051  ltnegcon1  7056  lenegcon1  7059  addge02  7066  leaddle0  7070  apreap  7174  prodgt02  7402  prodge02  7404  ltmulgt12  7414  lemulge12  7416  ltdivmul  7425  ledivmul  7426  ltdivmul2  7427  lt2mul2div  7428  ledivmul2  7429  ltrec  7432  ltrec1  7437  ltdiv23  7441  lediv23  7442  nnge1  7520  halfpos  7734  lt2halves  7738  addltmul  7739  avglt2  7742  avgle2  7744  zltlem1  7871  gtndiv  7899  qapne  8056