Theorem breq2d 2620

Description: Equality deduction for a binary relation.

Hypothesis

Ref	Expression
breq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
breq2d	|- (ph -> (CRA <-> CRB))

Proof of Theorem breq2d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 |- (ph -> A = B)
2		breq2 2613	. 2 |- (A = B -> (CRA <-> CRB))
3	1, 2	syl 10	1 |- (ph -> (CRA <-> CRB))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953   class class class wbr 2609

This theorem is referenced by:  breq12d 2621  breqtrd 2629  sbcbr1g 2654  isorel 3879  isocnv 3881  isotr 3882  isotrALT 3883  f1owe 3890  f1oweALT 3891  caoprord 4042  th3qlem2 4299  xpdom1g 4424  unidomg 4781  sdomsdomcard 4820  alephordi 4846  ltapq 5048  ltmpq 5049  addclprlem1 5090  mulclprlem 5093  1idpr 5105  ltaprlem 5122  ltapr 5123  prlem936a 5125  prlem936 5127  ltasr 5181  mulgt0sr 5186  sqgt0sr 5187  ssgt0sr 5189  pre-axltadd 5261  pre-axmulgt0 5262  addge0 5573  addgegt0 5574  msqgt0t 5589  msqge0t 5590  ltadd1t 5597  leadd1t 5599  ltsubaddt 5601  ltsubadd2t 5602  lesubaddt 5603  lesubadd2t 5604  lt2addt 5617  le2addt 5618  addgt0t 5620  addgegt0t 5621  addge0t 5623  ltaddpos2t 5625  posdift 5627  ltnegt 5628  ltnegcon1t 5629  lenegt 5630  lenegcon1t 5631  addge02t 5646  suble0t 5648  lesub0t 5651  mulge0t 5652  prodgt0 5775  prodgt0t 5782  prodgt02t 5783  prodge0t 5784  prodge02t 5785  ltmul1t 5786  ltmulgt12t 5803  ltdiv1t 5805  ltmuldivt 5817  ltdivmult 5819  ledivmult 5820  ltdivmul2t 5821  lt2mul2divt 5822  ledivmul2t 5823  ltrec 5827  ltrect 5832  lerect 5833  lt2msqt 5834  ltrec1t 5836  ltdiv23t 5840  lediv23t 5841  le2msqt 5851  xrmax1 5857  max1ALT 5864  nnge1t 5891  nnleltp1t 5901  lt2halvest 5989  avglet 5991  nnreclt 6019  nn0ltlem1t 6076  zltp1let 6128  zltlem1t 6131  gtndivt 6140  rebtwnz 6170  flleltt 6175  flbit 6184  btwnzge0t 6188  qbtwnre 6216  monoord 6231  om2uzlt 6235  ser1mono 6274  expgt0t 6520  expge0t 6522  expgt1t 6523  sqge0t 6564  expnbndt 6585  discrlem2 6587  discrlem 6589  sqrlem21 6623  sqrgt0 6631  sqrgt0t 6641  sqrge0t 6642  sqrlet 6643  cjmulge0t 6738  absge0t 6789  absgt0t 6831  abs3lemt 6844  facwordit 6881  2climnn 7039  2climnn0 7040  climge0 7049  climaddlem3 7052  climmulc2 7065  caucvglem2 7094  caucvg 7099  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  iserzgt0 7146  ivthlem6 7221  ivthlem6OLD 7230  efcltlem1 7246  abspef01tlub 7336  efgt0t 7346  efcnlem4 7362  reefiso 7370  znnen 7445  ruclem4 7456  ruclem32 7484  mettri2 7752  mettri4 7753  lmuni 7886  lmle 7895  metcn4i 7906  xplmi2 7908  bopcnlem3 7917  lmcau 7930  bcthlem1 7933  bcthlem15 7947  bcthlem25 7957  isblo3i 8392  blo3i 8393  blocnilem 8395  siilem2 8443  minveclem24 8499  pilem1 8590  sincosq1sgn 8621  sincosq2sgn 8622  sincosq4sgn 8624  logltbt 8698  logltbtOLD 8715  normlem6 8902  normgt0tOLD 8914  normgt0t 8915  norm3dift 8938  norm3lemt 8940  hlimcaui 9027  projlem7 9108  projlem16 9117  projlem17 9118  projlem20 9121  projlem28 9129  pjthlem9 9142  pjthlem12 9145  pjige0t 9553  lnopcon 9878  lnopcnbdt 9880  lnfncon 9905  lnfncnbdt 9907  riesz1t 9913  cnlnadjlem2 9916  cnlnadjlem8 9922  leopg 9967  leop2t 9969  leoppost 9971  leopaddt 9977  leopmulit 9978  leopmul2it 9980  pjssge0t 10005  pjdifnormt 10006  pjsspos 10011  pjssdif1 10014  stelt 10051  stge0t 10061  chcv1t 10190  cvexcht 10209  atcvatlem 10220  atcvat3 10231  atdmd 10233  cdj3 10273  abs2sqlet 10279  abs2sqltt 10280  iintlem1 10476

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610

Copyright terms: Public domain