Theorem breq1d 2619

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 2612	. 2 |- (A = B -> (ARC <-> BRC))
3	1, 2	syl 10	1 |- (ph -> (ARC <-> BRC))

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

This theorem is referenced by:  breq12d 2621  eqbrtrd 2625  syl6eqbr 2642  sbcbr2g 2655  isorel 3879  isocnv 3881  isotr 3882  isotrALT 3883  f1owe 3890  f1oweALT 3891  caoprord 4042  th3qlem2 4299  ensn1g 4406  xpsneng 4416  xpdom2 4422  pwen 4483  unifi 4532  iunfi 4543  pwfi 4545  pm54.43 4546  suppr 4562  uniimadomf 4783  iundom 4784  alephordi 4846  alephval2 4874  ltapq 5048  ltmpq 5049  prlem936a 5125  prlem936 5127  ltasr 5181  addgt0sr 5185  pre-axltadd 5261  ltadd1t 5597  leadd1t 5599  ltsubaddt 5601  lesubaddt 5603  ltaddsub2t 5606  leaddsub2t 5608  lt2addt 5617  le2addt 5618  ltaddpost 5624  ltnegt 5628  lenegt 5630  lenegcon2t 5632  addge01t 5645  ltmuldiv 5781  ltmul1t 5786  mulgt1t 5801  ltmulgt11t 5802  ltdiv1t 5805  gt0divt 5807  ge0divt 5808  ltmuldivt 5817  ltmuldiv2t 5818  lemuldiv2t 5825  ltrec 5827  lt2msq 5829  ltrect 5832  lerect 5833  lt2msqt 5834  lerec2t 5837  ltdiv23t 5840  lediv23t 5841  le2msqt 5851  xrmin2 5860  nnleltp1t 5901  avglet 5991  nn0ltp1let 6074  zltp1let 6128  zlem1ltt 6130  flleltt 6175  fsequb 6455  seqzfval 6469  exple1t 6538  sqlecant 6572  discrlem2 6587  discrlem3 6588  sqr0 6602  sqrlem4 6606  sqrlem6 6608  sqrlem12 6614  sqrlem22 6624  sqrlem24 6626  sqrgt0i 6627  sqrlem26 6628  sqrlet 6643  sqr2irr 6659  absltt 6817  abslttOLD 6818  abslet 6819  abssubne0t 6820  absdifltt 6821  absdiflet 6822  lenegsqt 6823  abs3lemt 6844  seq1bnd 6847  seq1ublem 6848  cau2 6850  clim 6915  sumeq2 6923  serzcmp0 6993  clm0 7021  clmnns 7022  clm0nns 7023  clm0i 7027  climfnn 7030  climconst 7031  climconst3 7033  climunii 7035  climshft 7041  climres 7042  serzclim0 7046  climrecl 7047  climge0 7049  climaddlem3 7052  climmullem8 7063  climcmpc1 7075  iserzcmp0 7079  iserzex 7082  climubi 7089  climub 7090  climsup 7091  climcau 7092  caucvglem2 7094  caucvg 7099  caucvg3t 7104  serzf0 7105  ser1f0 7106  ser1clim0 7109  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  dfisum 7127  isumvalt 7128  isumclim3t 7135  isumclim5t 7137  reccnv 7153  infcvglem1 7156  expcnvlem3 7164  expcnvlem5 7166  expcnvlem6 7167  expcnv 7168  geolim 7172  geolim1 7174  cvgratlem2 7186  elcncf 7200  negfcncf 7204  rescncf 7207  mulc1cncf 7214  ivthlem1 7216  ivthlem4 7219  ivthlem6 7221  ivthlem7 7222  ivthlem8 7223  ivthlem9 7224  isupivth 7225  ivthlem4OLD 7228  ivthlem6OLD 7230  ivthlem7OLD 7231  ivthlem8OLD 7232  ivth2OLD 7234  efseq1ex 7248  efaddlem24 7303  efaddlem27 7306  eftlext 7320  ef1tlub 7324  abspef01tlub 7336  efcnlem4 7362  reefiso 7370  ruclem4 7456  ruclem32 7484  ruclem33 7485  ruclem35 7487  infxpdom 7514  fctop 7592  cctop 7594  blfval 7775  blval 7777  elbl 7778  elbl3 7780  blss 7793  metcnp2 7827  metcni 7833  metcnss 7837  metcnss2 7838  cncfmet 7844  bl2ioo 7850  lmbr 7866  iscau 7874  iscau3 7876  lmcvgnns 7879  lmss 7888  caussi 7889  causs 7890  lmfexlem3 7893  lmle 7895  lmclim 7898  metelcls 7900  metcnp4lem2 7903  metcnp4 7904  metcn4i 7906  xplmi 7907  xplm 7909  xpcn 7910  iscms2lem3 7925  iscms2lem4 7926  lmcau 7930  cncms 7932  bcthlem2 7934  bcthlem29 7961  isnvlem 8167  isnvgOLD 8168  nvi 8173  nvelbl 8263  nvelbl2 8264  nvcni 8266  nvlmle 8268  nmcnilem 8272  va1cnlem 8279  sm1cnilem 8281  nvcnpi4 8355  nmofval 8357  nmosetn0 8360  nmolb 8366  nmoubi 8367  nmobndseqi 8372  bloval 8373  isblo 8374  nmo0 8383  nmlno0lem 8385  blocnilem 8395  siilem2 8443  ubthlem1 8460  ubthi 8475  minveclem9 8484  minveclem24 8499  minveclem27 8502  minveclem28 8503  minveclem39 8518  sincosq2sgn 8622  sincosq3sgn 8623  sincosq4sgn 8624  logltbt 8698  logltbtOLD 8715  h2hcau 8788  h2hlm 8789  normlem7tALT 8906  norm3lemt 8940  hcau 8972  hcau2 8976  hlim 8977  hlim2 8981  hhcms 8993  hlim0 9026  hlimcaui 9027  hlimunii 9029  hhsscms 9067  occllem6 9094  projlem1 9102  projlem2 9103  projlem7 9108  projlem17 9118  projlem20 9121  projlem25 9126  projlem26 9127  projlem31 9132  pjth 9148  cmcm3t 9475  pjnormt 9586  pjnelt 9588  elcnopt 9700  elbdopt 9704  nmopsetn0 9709  nmfnsetn0 9722  elcnfnt 9726  nmoplbt 9748  nmopubt 9749  cnopct 9753  nmfnlbt 9764  nmfnleubt 9765  cnfnct 9770  0cnop 9819  0cnfn 9820  idcnop 9821  nmop0 9826  nmfn0 9827  nmlnop0ALT 9835  nmcopexlem2 9867  nmcopexlem4 9869  nmcopexlem6 9871  nmcopex 9872  lnopcont 9879  nmcfnexlem2 9896  nmcfnexlem4 9898  nmcfnexlem6 9900  nmcfnex 9901  lnfncont 9906  nlelch 9909  branmfnt 9951  leop3t 9970  hmopidmch 9990  stelt 10051  stle1t 10062  cvmdt 10171  cvdmdt 10172  cvexcht 10209  cdj3 10273  abs2sqlet 10279  abs2sqltt 10280  mslb1 10473  msra3 10475

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