Theorem breq2d 2703

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

Syntax hints:   -> wi 3   <-> wb 144   = wceq 992   class class class wbr 2692

This theorem is referenced by:  breq12d 2704  breqtrd 2712  sbcbr1g 2738  isorel 4008  isocnv 4010  isotr 4011  isotrALT 4012  f1owe 4019  f1oweALT 4020  caoprord 4117  th3qlem2 4456  xpdom1g 4585  unidomg 4955  sdomsdomcard 4998  alephordi 5024  cdaeng 5076  nnacda 5090  ltapq 5230  ltmpq 5231  addclprlem1 5272  mulclprlem 5275  1idpr 5287  ltaprlem 5304  ltapr 5305  prlem936a 5307  prlem936 5309  ltasr 5363  mulgt0sr 5368  sqgt0sr 5369  ssgt0sr 5371  pre-axltadd 5443  pre-axmulgt0 5444  addge0i 5753  addgegt0i 5754  msqgt0 5769  msqge0 5770  ltadd1 5777  leadd1 5779  ltsubadd 5781  ltsubadd2 5782  lesubadd 5783  lesubadd2 5784  lt2add 5797  le2add 5798  addgt0 5801  addgegt0 5802  addge0 5804  ltaddpos2 5806  posdif 5808  ltneg 5809  ltnegcon1 5810  leneg 5811  lenegcon1 5812  addge02 5827  suble0 5829  lesub0 5832  mulge0 5833  mulge0OLD 5834  prodgt0i 5959  prodgt0 5966  prodgt02 5967  prodge0 5968  prodge02 5969  ltmul1 5970  ltmulgt12 5991  ltdiv1 5993  ltdiv1OLD 5994  ltmuldiv 6007  ltmuldivOLD 6008  ltdivmul 6011  ltdivmulOLD 6012  ledivmul 6013  ledivmulOLD 6014  ltdivmul2 6015  lt2mul2div 6016  lt2mul2divOLD 6017  ledivmul2 6018  ledivmul2OLD 6019  ltreci 6024  ltrec 6029  lerec 6030  lt2msq 6031  ltrec1 6033  ltdiv23 6037  lediv23 6038  le2msq 6048  xrmax1 6054  max1ALT 6061  nnge1 6088  nnleltp1 6100  lt2halves 6188  avgle 6190  nnrecl 6240  nn0ltlem1 6297  zltp1le 6349  zltlem1 6352  gtndiv 6364  rebtwnz 6394  qbtwnre 6418  fllelt 6426  flbi 6439  btwnzge0 6445  monoord 6482  fz01en 6623  om2uzlti 6661  ser1monoi 6702  expgt0 6783  expge0 6785  expgt1 6786  sqge0 6830  expnbnd 6852  discrlem2 6858  discrlem 6860  sqrlem21 6894  sqrgt0i 6902  sqrgt0 6912  sqrge0 6913  sqrle 6914  cjmulge0 7004  absge0 7056  absgt0 7096  abs3lem 7110  facwordi 7147  2climnn 7305  2climnn0 7306  climge0 7315  climaddlem3 7319  climmulc2 7332  caucvglem2 7361  caucvgi 7366  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  iserzgt0 7415  explecnv 7438  ivthlem6 7491  efcltlem1 7509  abspef01tlubi 7603  efgt0 7613  efcnlem4 7630  reefiso 7636  znnen 7714  ruclem4 7725  ruclem32 7753  mettri2 8023  mettri4 8024  lmuni 8162  lmle 8171  metcn4i 8183  xplmi2 8185  bopcnlem3 8194  lmcau 8207  bcthlem1 8210  bcthlem15 8224  bcthlem25 8234  vacnlem6 8587  nmounbseqi 8694  isblo3i 8716  blo3i 8717  blocnilem 8719  siilem2 8768  minveclem24 8828  pilem1 8938  sincosq1sgn 8971  sincosq2sgn 8972  sincosq4sgn 8974  logltb 9048  normlem6 9257  normgt0OLD 9269  normgt0 9270  norm3dif 9293  norm3lemt 9295  hlimcauii 9382  projlem7 9468  projlem16 9477  projlem17 9478  projlem20 9481  projlem28 9489  pjthlem9 9503  pjthlem12 9506  pjige0 9914  lnopconi 10242  lnopcnbd 10244  lnfnconi 10269  lnfncnbd 10271  riesz1 10277  cnlnadjlem2 10280  cnlnadjlem8 10286  leopg 10335  leop2 10337  leoppos 10339  leopadd 10345  leopmuli 10346  leopmul2i 10348  pjssge0i 10374  pjdifnormi 10375  pjssposi 10380  pjssdif1i 10383  stel 10422  stge0 10432  chcv1 10563  cvexch 10582  atcvatlem 10594  atcvat3i 10605  atdmd 10607  cdj3i 10650  abs2sqlet 10659  abs2sqltt 10660  iintlem1 11155  omsubsdomlem2 11441  elomsubsd 11446  infenomsub 11450  fnejoin1 11591  ufilen 11664  seqpo 11878  incsequz2 11880  fsumleisumi 11889  fsumlt1 11894  blhalf 11911  geomcau 11914  iihalf2 11937  heiborlem16 12026  bfplem6 12059  bfp 12065  recms 12066

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102  df-sn 2470  df-pr 2471  df-op 2474  df-br 2693

Copyright terms: Public domain