Theorem breq1d 2634

Description: Equality deduction for a binary relation.

Hypothesis

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

Assertion

Ref	Expression
breq1d	|- (ph -> (ARC <-> BRC))

Proof of Theorem breq1d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 |- (ph -> A = B)
2		breq1 2627	. 2 |- (A = B -> (ARC <-> BRC))
3	1, 2	syl 10	1 |- (ph -> (ARC <-> BRC))

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

This theorem is referenced by:  breq12d 2636  eqbrtrd 2640  syl6eqbr 2657  sbcbr2g 2670  isorel 3900  isocnv 3902  isotr 3903  isotrALT 3904  f1owe 3911  f1oweALT 3912  caoprord 4062  th3qlem2 4321  ensn1g 4431  xpsneng 4442  xpdom2 4448  pwen 4509  unifiOLD 4570  pwfiOLD 4580  pm54.43 4581  suppr 4599  uniimadomf 4821  iundom 4822  alephordi 4885  alephval2 4913  ltapq 5088  ltmpq 5089  prlem936a 5165  prlem936 5167  ltasr 5221  addgt0sr 5225  pre-axltadd 5301  ltadd1t 5635  leadd1t 5637  ltsubaddt 5639  lesubaddt 5641  ltaddsub2t 5644  leaddsub2t 5646  lt2addt 5655  le2addt 5656  ltaddpost 5663  ltnegt 5667  lenegt 5669  lenegcon2t 5671  addge01t 5684  ltmuldiv 5827  ltmul1t 5832  mulgt1t 5847  ltmulgt11t 5848  ltdiv1t 5851  ltdiv1tOLD 5852  gt0divt 5855  ge0divt 5856  ltmuldivt 5865  ltmuldivtOLD 5866  ltmuldiv2t 5867  ltmuldiv2tOLD 5868  lemuldiv2t 5878  lemuldiv2tOLD 5879  ltrec 5881  lt2msq 5883  ltrect 5886  lerect 5887  lt2msqt 5888  lerec2t 5891  ltdiv23t 5894  lediv23t 5895  le2msqt 5905  xrmin2 5914  nnleltp1t 5956  avglet 6046  nn0ltp1let 6129  zltp1let 6183  zlem1ltt 6185  flleltt 6230  fsequb 6524  seqzfval 6538  exple1t 6608  sqlecant 6642  discrlem2 6658  discrlem3 6659  sqr0 6673  sqrlem4 6677  sqrlem6 6679  sqrlem12 6685  sqrlem22 6695  sqrlem24 6697  sqrgt0i 6698  sqrlem26 6699  sqrlet 6714  sqr2irr 6730  absltt 6880  abslet 6881  abssubne0t 6882  absdifltt 6883  absdiflet 6884  lenegsqt 6885  abs3lemt 6907  seq1bnd 6910  seq1ublem 6911  cau2 6913  clim 6977  sumeq2 6985  serzcmp0 7055  clm0 7083  clmnns 7084  clm0nns 7085  clm0i 7089  climfnn 7092  climconst 7094  climconst3 7096  climunii 7098  climshft 7104  climres 7105  serzclim0 7109  climrecl 7110  climge0 7112  climabs0 7113  climaddlem3 7116  climmullem8 7127  climcmpc1 7139  iserzcmp0 7143  iserzex 7146  climubi 7153  climub 7154  climsup 7155  climcau 7156  caucvglem2 7158  caucvg 7163  caucvg3t 7168  serzf0 7169  ser1f0 7170  ser1clim0 7173  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  dfisum 7191  isumvalt 7192  isumclim3t 7200  isumclim5t 7202  reccnv 7218  infcvglem1 7221  expcnvlem3 7229  expcnvlem5 7231  expcnvlem6 7232  expcnv 7233  geolim 7237  geolim1 7239  cvgratlem2 7251  elcncf 7265  negfcncf 7269  rescncf 7272  mulc1cncf 7279  ivthlem1 7281  ivthlem4 7284  ivthlem6 7286  ivthlem7 7287  ivthlem8 7288  ivthlem9 7289  isupivth 7290  efseq1ex 7306  efaddlem24 7361  efaddlem27 7364  eftlext 7378  ef1tlub 7382  abspef01tlub 7395  efcnlem4 7422  reefiso 7428  ruclem4 7514  ruclem32 7542  ruclem33 7543  ruclem35 7545  infxpdom 7572  fctopOLD 7647  cctop 7649  blfval 7832  blval 7834  elbl 7835  elbl3 7837  blss 7850  metcnp2 7885  metcni 7891  metcnss 7895  metcnss2 7896  cncfmet 7902  bl2ioo 7908  lmbr 7925  iscau 7933  iscau3 7935  iscau4 7937  lmbrnns 7939  lmcvgnns 7940  iscaunns 7941  lmss 7950  caussi 7951  causs 7952  lmfexlem3 7955  lmle 7957  lmclim 7960  metelcls 7962  metcnp4lem2 7966  metcnp4 7967  metcn4i 7969  xplmi 7970  xplm 7972  xpcn 7973  iscms2lem3 7988  iscms2lem4 7989  lmcau 7993  cncms 7995  bcthlem2 7997  bcthlem29 8024  isnvlem 8225  nvi 8229  nvelbl 8321  nvelbl2 8322  nvcni 8325  nvcni2 8326  nvcni3 8327  nvlmle 8329  nmcnilem 8333  va1cnlem 8341  sm1cnilem 8343  nvcnpi3 8418  nvcnpi4 8419  nmofval 8421  nmosetn0 8424  nmolb 8430  nmoubi 8431  nmobndseqi 8436  bloval 8437  isblo 8438  nmo0 8447  nmlno0lem 8449  blocnilem 8460  siilem2 8508  ubthlem1 8525  ubthi 8540  minveclem9 8549  minveclem24 8564  minveclem27 8567  minveclem28 8568  minveclem39 8583  sincosq2sgn 8700  sincosq3sgn 8701  sincosq4sgn 8702  logltbt 8771  h2hcau 8844  h2hlm 8845  normlem7tALT 8980  norm3lemt 9014  hcau 9046  hcau2 9050  hlim 9051  hlim2 9055  hhcms 9067  hlim0 9100  hlimcaui 9101  hlimunii 9103  hhsscms 9145  occllem6 9173  projlem1 9181  projlem2 9182  projlem7 9187  projlem17 9197  projlem20 9200  projlem25 9205  projlem26 9206  projlem31 9211  pjth 9228  cmcm3t 9553  pjnormt 9664  pjnelt 9666  elcnopt 9778  elbdopt 9782  nmopsetn0 9787  nmfnsetn0 9800  elcnfnt 9804  nmoplbt 9826  nmopubt 9827  cnopct 9832  nmfnlbt 9843  nmfnleubt 9844  cnfnct 9849  0cnop 9898  0cnfn 9899  idcnop 9900  nmop0 9905  nmfn0 9906  nmlnop0ALT 9915  nmcopexlem2 9947  nmcopexlem4 9949  nmcopexlem6 9951  nmcopex 9952  lnopcont 9959  nmcfnexlem2 9976  nmcfnexlem4 9978  nmcfnexlem6 9980  nmcfnex 9981  lnfncont 9986  nlelch 9989  branmfnt 10033  leop3t 10053  hmopidmch 10074  stelt 10136  stle1t 10147  cvmdt 10258  cvdmdt 10259  cvexcht 10296  cdj3 10363  abs2sqlet 10369  abs2sqltt 10370  nndivlub 10417  mslb1 10600  msra3 10602

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