Theorem breq1d 2597

Description: Equality deduction for 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 2590	. 2 |- (A = B -> (ARC <-> BRC))
3	1, 2	syl 10	1 |- (ph -> (ARC <-> BRC))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 1099   class class class wbr 2587

This theorem is referenced by:  breq12d 2599  eqbrtrd 2603  syl6eqbr 2620  sbcbr2g 2633  isorel 3833  isocnv 3835  isotr 3836  isotrALT 3837  f1owe 3844  f1oweALT 3845  caoprord 3996  th3qlem2 4253  ensn1g 4360  xpsneng 4370  xpdom2 4376  pwen 4435  unifi 4484  iunfi 4495  pwfi 4497  pm54.43 4498  suppr 4514  uniimadomf 4735  iundom 4736  alephordi 4797  alephval2 4825  ltapq 4999  ltmpq 5000  prlem936a 5076  prlem936 5078  ltasr 5132  addgt0sr 5136  pre-axltadd 5212  ltadd1t 5548  leadd1t 5550  ltsubaddt 5552  lesubaddt 5554  ltaddsub2t 5557  leaddsub2t 5559  lt2addt 5568  le2addt 5569  ltaddpost 5575  ltnegt 5579  lenegt 5581  lenegcon2t 5583  addge01t 5596  ltmuldiv 5732  ltmul1t 5737  mulgt1t 5752  ltmulgt11t 5753  ltdiv1t 5756  gt0divt 5758  ge0divt 5759  ltmuldivt 5768  ltmuldiv2t 5769  lemuldiv2t 5776  ltrec 5778  lt2msq 5780  ltrect 5783  lerect 5784  lt2msqt 5785  lerec2t 5788  ltdiv23t 5791  lediv23t 5792  le2msqt 5802  xrmin2 5811  nnleltp1t 5852  avglet 5942  nn0ltp1let 6025  zltp1let 6079  zlem1ltt 6081  flleltt 6126  fsequb 6406  seqzfval 6420  exple1t 6489  sqlecant 6523  discrlem2 6538  discrlem3 6539  sqr0 6553  sqrlem4 6557  sqrlem6 6559  sqrlem12 6565  sqrlem22 6575  sqrlem24 6577  sqrgt0i 6578  sqrlem26 6579  sqrlet 6594  sqr2irr 6610  absltt 6768  abslttOLD 6769  abslet 6770  abssubne0t 6771  absdifltt 6772  absdiflet 6773  lenegsqt 6774  abs3lemt 6795  seq1bnd 6798  seq1ublem 6799  cau2 6801  clim 6866  sumeq2 6874  serzcmp0 6944  clm0 6972  clmnns 6973  clm0nns 6974  clm0i 6978  climfnn 6981  climconst 6982  climconst3 6984  climunii 6986  climshft 6992  climres 6993  serzclim0 6997  climrecl 6998  climge0 7000  climaddlem3 7003  climmullem8 7014  climcmpc1 7026  iserzcmp0 7030  iserzex 7033  climubi 7040  climub 7041  climsup 7042  climcau 7043  caucvglem2 7045  caucvg 7050  caucvg3t 7055  serzf0 7056  ser1f0 7057  ser1clim0 7060  cvgcmp3cetlem1 7075  cvgcmp3cetlem2 7076  dfisum 7078  isumvalt 7079  isumclim3t 7086  isumclim5t 7088  reccnv 7104  infcvglem1 7107  expcnvlem3 7115  expcnvlem5 7117  expcnvlem6 7118  expcnv 7119  geolim 7123  geolim1 7125  cvgratlem2 7137  elcncf 7151  negfcncf 7155  rescncf 7158  mulc1cncf 7165  ivthlem1 7167  ivthlem4 7170  ivthlem6 7172  ivthlem7 7173  ivthlem8 7174  ivthlem9 7175  isupivth 7176  ivthlem4OLD 7179  ivthlem6OLD 7181  ivthlem7OLD 7182  ivthlem8OLD 7183  ivth2OLD 7185  efseq1ex 7199  efaddlem24 7254  efaddlem27 7257  eftlext 7271  ef1tlub 7275  abspef01tlub 7287  efcnlem4 7313  reefiso 7321  ruclem4 7407  ruclem32 7435  ruclem33 7436  ruclem35 7438  infxpdom 7465  fctop 7543  cctop 7545  blfval 7723  blval 7725  elbl 7726  elbl3 7728  blss 7741  metcnp2 7775  metcni 7781  metcnss 7785  metcnss2 7786  cncfmet 7792  bl2ioo 7798  lmbr 7814  iscau 7822  iscau3 7824  lmcvgnns 7827  lmss 7836  caussi 7837  causs 7838  lmfexlem3 7841  lmle 7843  lmclim 7846  metelcls 7848  metcnp4lem2 7851  metcnp4 7852  metcn4i 7854  xplmi 7855  xplm 7857  xpcn 7858  iscms2lem3 7873  iscms2lem4 7874  lmcau 7878  cncms 7880  bcthlem2 7882  bcthlem29 7909  isnvg 8109  nvi 8111  nvelbl 8200  nvelbl2 8201  nvcni 8203  nvlmle 8205  nmcnilem 8209  va1cnlem 8214  sm1cnilem 8216  nvcnpi4 8290  nmofval 8292  nmosetn0 8295  nmolb 8301  nmoubi 8302  nmobndseqi 8307  bloval 8308  isblo 8309  nmo0 8318  nmlno0lem 8320  blocnilem 8330  siilem2 8378  ubthlem1 8395  ubthi 8410  minveclem9 8419  minveclem24 8434  minveclem27 8437  minveclem28 8438  minveclem39 8453  sincosq2sgn 8535  sincosq3sgn 8536  sincosq4sgn 8537  logltbt 8611  logltbtOLD 8628  abs2sqlet 8641  abs2sqltt 8642  mslb1 8823  msra3 8825  normlem7tALT 9134  norm3lemt 9168  hcau 9201  hcau2 9205  hlim 9207  hlim2 9211  hillim 9216  hilcau 9217  hhcms 9223  hlim0 9256  hlimcaui 9257  hlimunii 9259  occllem6 9308  projlem1 9316  projlem2 9317  projlem7 9322  projlem17 9332  projlem20 9335  projlem25 9340  projlem26 9341  projlem31 9346  pjth 9362  cmcm3t 9689  pjnormt 9800  pjnelt 9802  elcnopt 9914  elbdopt 9918  nmopsetn0 9923  nmfnsetn0 9936  elcnfnt 9940  nmoplbt 9962  nmopubt 9963  cnopct 9967  nmfnlbt 9978  nmfnleubt 9979  cnfnct 9984  0cnop 10033  0cnfn 10034  idcnop 10035  nmop0 10040  nmfn0 10041  nmlnop0ALT 10049  nmcopexlem2 10081  nmcopexlem4 10083  nmcopexlem6 10085  nmcopex 10086  lnopcont 10093  nmcfnexlem2 10110  nmcfnexlem4 10112  nmcfnexlem6 10114  nmcfnex 10115  lnfncont 10120  nlelch 10123  branmfnt 10165  leop3t 10184  hmopidmch 10204  stelt 10265  stle1t 10276  cvmdt 10385  cvdmdt 10386  cvexcht 10423  cdj3 10487

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787  df-un 2021  df-sn 2383  df-pr 2384  df-op 2387  df-br 2588

Copyright terms: Public domain