Theorem breq2d 2635

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 2628	. 2 |- (A = B -> (CRA <-> CRB))
3	1, 2	syl 10	1 |- (ph -> (CRA <-> CRB))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 958   class class class wbr 2624

This theorem is referenced by:  breq12d 2636  breqtrd 2644  sbcbr1g 2669  isorel 3900  isocnv 3902  isotr 3903  isotrALT 3904  f1owe 3911  f1oweALT 3912  caoprord 4062  th3qlem2 4321  xpdom1g 4450  unidomg 4819  sdomsdomcard 4859  alephordi 4885  ltapq 5088  ltmpq 5089  addclprlem1 5130  mulclprlem 5133  1idpr 5145  ltaprlem 5162  ltapr 5163  prlem936a 5165  prlem936 5167  ltasr 5221  mulgt0sr 5226  sqgt0sr 5227  ssgt0sr 5229  pre-axltadd 5301  pre-axmulgt0 5302  addge0 5611  addgegt0 5612  msqgt0t 5627  msqge0t 5628  ltadd1t 5635  leadd1t 5637  ltsubaddt 5639  ltsubadd2t 5640  lesubaddt 5641  lesubadd2t 5642  lt2addt 5655  le2addt 5656  addgt0t 5659  addgegt0t 5660  addge0t 5662  ltaddpos2t 5664  posdift 5666  ltnegt 5667  ltnegcon1t 5668  lenegt 5669  lenegcon1t 5670  addge02t 5685  suble0t 5687  lesub0t 5690  mulge0t 5691  prodgt0 5821  prodgt0t 5828  prodgt02t 5829  prodge0t 5830  prodge02t 5831  ltmul1t 5832  ltmulgt12t 5849  ltdiv1t 5851  ltdiv1tOLD 5852  ltmuldivt 5865  ltmuldivtOLD 5866  ltdivmult 5869  ltdivmultOLD 5870  ledivmultOLD 5871  ltdivmul2t 5872  ltdivmul2tOLD 5873  lt2mul2divt 5874  ledivmul2tOLD 5875  ltrec 5881  ltrect 5886  lerect 5887  lt2msqt 5888  ltrec1t 5890  ltdiv23t 5894  lediv23t 5895  le2msqt 5905  xrmax1 5911  max1ALT 5918  nnge1t 5945  nnleltp1t 5956  lt2halvest 6044  avglet 6046  nnreclt 6074  nn0ltlem1t 6131  zltp1let 6183  zltlem1t 6186  gtndivt 6195  rebtwnz 6224  flleltt 6230  flbit 6242  btwnzge0t 6247  qbtwnre 6279  monoord 6295  om2uzlt 6299  ser1mono 6338  expgt0t 6590  expge0t 6592  expgt1t 6593  sqge0t 6634  expnbndt 6655  discrlem2 6658  discrlem 6660  sqrlem21 6694  sqrgt0 6702  sqrgt0t 6712  sqrge0t 6713  sqrlet 6714  cjmulge0t 6803  absge0t 6854  absgt0t 6893  abs3lemt 6907  facwordit 6944  2climnn 7102  2climnn0 7103  climge0 7112  climaddlem3 7116  climmulc2 7129  caucvglem2 7158  caucvg 7163  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  iserzgt0 7211  ivthlem6 7286  efcltlem1 7304  abspef01tlub 7395  efgt0t 7405  efcnlem4 7422  reefiso 7428  znnen 7503  ruclem4 7514  ruclem32 7542  mettri2 7810  mettri4 7811  lmuni 7948  lmle 7957  metcn4i 7969  xplmi2 7971  bopcnlem3 7980  lmcau 7993  bcthlem1 7996  bcthlem15 8010  bcthlem25 8020  isblo3i 8457  blo3i 8458  blocnilem 8460  siilem2 8508  minveclem24 8564  pilem1 8666  sincosq1sgn 8699  sincosq2sgn 8700  sincosq4sgn 8702  logltbt 8771  normlem6 8976  normgt0tOLD 8988  normgt0t 8989  norm3dift 9012  norm3lemt 9014  hlimcaui 9101  projlem7 9187  projlem16 9196  projlem17 9197  projlem20 9200  projlem28 9208  pjthlem9 9222  pjthlem12 9225  pjige0t 9631  lnopcon 9958  lnopcnbdt 9960  lnfncon 9985  lnfncnbdt 9987  riesz1t 9993  cnlnadjlem2 9996  cnlnadjlem8 10002  leopg 10050  leop2t 10052  leoppost 10054  leopaddt 10060  leopmulit 10061  leopmul2it 10063  pjssge0t 10089  pjdifnormt 10090  pjsspos 10095  pjssdif1 10098  stelt 10136  stge0t 10146  chcv1t 10277  cvexcht 10296  atcvatlem 10307  atcvat3 10318  atdmd 10320  cdj3 10363  abs2sqlet 10369  abs2sqltt 10370  iintlem1 10603

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2053  df-sn 2416  df-pr 2417  df-op 2420  df-br 2625

Copyright terms: Public domain