Theorem breq1d 2702

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

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

This theorem is referenced by:  breq12d 2704  eqbrtrd 2708  syl6eqbr 2725  sbcbr2g 2739  isorel 4008  isocnv 4010  isotr 4011  isotrALT 4012  f1owe 4019  f1oweALT 4020  caoprord 4117  fparlem1 4199  fparlem2 4200  th3qlem2 4456  ensn1g 4566  xpsneng 4577  xpdom2 4583  pwen 4650  pm54.43 4715  suppr 4733  uniimadomf 4957  iundom 4958  alephordi 5024  alephval2 5052  cdaeng 5076  nnaun 5091  ltapq 5230  ltmpq 5231  prlem936a 5307  prlem936 5309  ltasr 5363  addgt0sr 5367  pre-axltadd 5443  ltadd1 5777  leadd1 5779  ltsubadd 5781  lesubadd 5783  ltaddsub2 5786  leaddsub2 5788  lt2add 5797  le2add 5798  ltaddpos 5805  ltneg 5809  leneg 5811  lenegcon2 5813  addge01 5826  ltmuldivi 5965  ltmul1 5970  mulgt1 5989  ltmulgt11 5990  ltdiv1 5993  ltdiv1OLD 5994  gt0div 5997  ge0div 5998  ltmuldiv 6007  ltmuldivOLD 6008  ltmuldiv2 6009  ltmuldiv2OLD 6010  lemuldiv2 6021  lemuldiv2OLD 6022  ltreci 6024  lt2msqi 6026  ltrec 6029  lerec 6030  lt2msq 6031  lerec2 6034  ltdiv23 6037  lediv23 6038  le2msq 6048  xrmin2 6057  nnleltp1 6100  avgle 6190  nn0ltp1le 6295  zltp1le 6349  zlem1lt 6351  fllelt 6426  fsequb 6654  seqzfval 6732  exple1 6804  sqlecan 6838  discrlem2 6858  discrlem3 6859  sqr0 6873  sqrlem4 6877  sqrlem6 6879  sqrlem12 6885  sqrlem22 6895  sqrlem24 6897  sqrgt0ii 6898  sqrlem26 6899  sqrle 6914  sqr2irr 6930  abslt 7083  absle 7084  abssubne0 7085  absdiflt 7086  absdifle 7087  lenegsq 7088  abs3lem 7110  seq1bndi 7113  seq1ublem 7114  cau2i 7116  clim 7180  sumeq2 7188  serzcmp0 7258  clm0i 7286  clmnnsi 7287  clm0nnsi 7288  clm0ii 7292  climfnn 7295  climconsti 7297  climconst3 7299  climunii 7301  climshfti 7307  climresi 7308  serzclim0 7312  climrecl 7313  climge0 7315  climabs0i 7316  climaddlem3 7319  climmullem8 7330  climcmpc1 7342  iserzcmp0 7346  iserzexi 7349  climubii 7356  climubi 7357  climsupi 7358  climcaui 7359  caucvglem2 7361  caucvgi 7366  caucvg3 7371  serzf0i 7372  ser1clim0 7376  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  dfisum 7395  isumval 7396  isumclim3 7404  isumclim5 7406  reccnv 7422  infcvglem1 7425  expcnvlem3 7433  expcnvlem5 7435  expcnvlem6 7436  expcnv 7437  geolim 7442  geolim1 7444  cvgratlem2 7456  elcncf 7470  negfcncfi 7474  rescncf 7477  mulc1cncf 7484  ivthlem1 7486  ivthlem4 7489  ivthlem6 7491  ivthlem7 7492  ivthlem8 7493  ivthlem9 7494  isupivthi 7495  efseq1ex 7511  efaddlem24 7566  efaddlem27 7569  eftlex 7583  ef1tlubi 7587  abspef01tlubi 7603  efcnlem4 7630  reefiso 7636  ruclem4 7725  ruclem32 7753  ruclem33 7754  ruclem35 7756  infxpdom 7783  cctop 7862  blfval 8045  blval 8047  elbl 8048  elbl3 8050  blss 8063  metcnp2 8099  metcni 8105  metcnss 8109  metcnss2 8110  cncfmet 8116  bl2ioo 8122  lmbr 8139  iscau 8147  iscau3 8149  iscau4 8151  lmbrnns 8153  lmcvgnns 8154  iscaunns 8155  lmss 8164  caussi 8165  causs 8166  lmfexlem3 8169  lmle 8171  lmclim 8174  metelcls 8176  metcnp4lem2 8180  metcnp4 8181  metcn4i 8183  xplmi 8184  xplm 8186  xpcn 8187  iscms2lem3 8202  iscms2lem4 8203  lmcau 8207  cncms 8209  bcthlem2 8211  bcthlem29 8238  isnvlem 8476  nvi 8480  nvelbl 8572  nvelbl2 8573  nvcni 8576  nvcni2 8577  nvcni3 8578  nvlmle 8580  vacnlem3 8584  nmcnilem 8591  va1cnlem 8599  sm1cnilem 8601  nvcnpi3 8676  nvcnpi4 8677  nmofval 8679  nmosetn0 8682  nmolb 8688  nmoubi 8689  nmounbseqi 8694  nmobndseqi 8695  bloval 8696  isblo 8697  nmo0 8706  nmlno0lem 8708  blocnilem 8719  siilem2 8768  ubthlem1 8787  ubthi 8804  minveclem9 8813  minveclem24 8828  minveclem27 8831  minveclem28 8832  minveclem39 8847  sincosq2sgn 8972  sincosq3sgn 8973  sincosq4sgn 8974  logltb 9048  h2hcau 9124  h2hlm 9125  normlem7tALT 9261  norm3lemt 9295  hcau 9327  hcau2 9331  hlimi 9332  hlim2 9336  hhcms 9348  hlim0 9381  hlimcauii 9382  hlimuniii 9384  hhsscms 9426  occllem6 9454  projlem1 9462  projlem2 9463  projlem7 9468  projlem17 9478  projlem20 9481  projlem25 9486  projlem26 9487  projlem31 9492  pjthi 9509  cmcm3 9834  pjnorm 9947  pjnel 9949  elcnop 10063  elbdop 10067  nmopsetn0 10072  nmfnsetn0 10085  elcnfn 10089  nmoplb 10111  nmopub 10112  cnopc 10117  nmfnlb 10128  nmfnleub 10129  cnfnc 10134  0cnop 10182  0cnfn 10183  idcnop 10184  nmop0 10189  nmfn0 10190  nmlnop0iALT 10199  nmcopexlem2 10231  nmcopexlem4 10233  nmcopexlem6 10235  nmcopexi 10236  lnopcon 10243  nmcfnexlem2 10260  nmcfnexlem4 10262  nmcfnexlem6 10264  nmcfnexi 10265  lnfncon 10270  nlelchi 10273  branmfn 10317  branmfnOLD 10318  leop3 10338  hmopidmchi 10359  stel 10422  stle1 10433  cvmd 10544  cvdmd 10545  cvexch 10582  cdj3i 10650  abs2sqlet 10659  abs2sqltt 10660  nndivlub 10707  mslb1 11152  msra3 11154  fictb 11423  infenomsub 11450  fnejoin2 11592  ufilen 11664  dif1en 11833  dif1card 11835  supubt 11855  seqpo 11878  incsequz2 11880  fsumltisumi 11886  fsumltisum 11887  fsumleisumi 11889  fsumleisum 11890  iserzshft2 11892  fsumlt1 11894  blssp 11908  geomcau 11914  lmclim2 11915  caushft 11916  caures 11917  addccncf 11945  sub1cncf 11946  sub2cncf 11947  ismtyhmeolem 12006  heiborlem16 12026  heiborlem18 12028  heiborlem34 12044  heiborlem35 12045  heiborlem36 12046  bfplem11 12064  rrndstprj2 12074  rrncms 12075

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