Theorem breq1d 2624

Description: Equality deduction for a binary relation.

Hypothesis

Ref	Expression
breq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
breq1d	⊢ (φ → (ARC ↔ BRC))

Proof of Theorem breq1d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (φ → A = B)
2		breq1 2617	. 2 ⊢ (A = B → (ARC ↔ BRC))
3	1, 2	syl 10	1 ⊢ (φ → (ARC ↔ BRC))

Syntax hints:   → wi 3   ↔ wb 146   = wceq 954   class class class wbr 2614

This theorem is referenced by:  breq12d 2626  eqbrtrd 2630  syl6eqbr 2647  sbcbr2g 2660  isorel 3885  isocnv 3887  isotr 3888  isotrALT 3889  f1owe 3896  f1oweALT 3897  caoprord 4048  th3qlem2 4305  ensn1g 4412  xpsneng 4422  xpdom2 4428  pwen 4489  unifi 4538  iunfi 4549  pwfi 4551  pm54.43 4552  suppr 4570  uniimadomf 4791  iundom 4792  alephordi 4854  alephval2 4882  ltapq 5056  ltmpq 5057  prlem936a 5133  prlem936 5135  ltasr 5189  addgt0sr 5193  pre-axltadd 5269  ltadd1t 5605  leadd1t 5607  ltsubaddt 5609  lesubaddt 5611  ltaddsub2t 5614  leaddsub2t 5616  lt2addt 5625  le2addt 5626  ltaddpost 5632  ltnegt 5636  lenegt 5638  lenegcon2t 5640  addge01t 5653  ltmuldiv 5789  ltmul1t 5794  mulgt1t 5809  ltmulgt11t 5810  ltdiv1t 5813  gt0divt 5815  ge0divt 5816  ltmuldivt 5825  ltmuldiv2t 5826  lemuldiv2t 5833  ltrec 5835  lt2msq 5837  ltrect 5840  lerect 5841  lt2msqt 5842  lerec2t 5845  ltdiv23t 5848  lediv23t 5849  le2msqt 5859  xrmin2 5868  nnleltp1t 5909  avglet 5999  nn0ltp1let 6082  zltp1let 6136  zlem1ltt 6138  flleltt 6183  fsequb 6463  seqzfval 6477  exple1t 6546  sqlecant 6580  discrlem2 6595  discrlem3 6596  sqr0 6610  sqrlem4 6614  sqrlem6 6616  sqrlem12 6622  sqrlem22 6632  sqrlem24 6634  sqrgt0i 6635  sqrlem26 6636  sqrlet 6651  sqr2irr 6667  absltt 6825  abslttOLD 6826  abslet 6827  abssubne0t 6828  absdifltt 6829  absdiflet 6830  lenegsqt 6831  abs3lemt 6852  seq1bnd 6855  seq1ublem 6856  cau2 6858  clim 6923  sumeq2 6931  serzcmp0 7001  clm0 7029  clmnns 7030  clm0nns 7031  clm0i 7035  climfnn 7038  climconst 7039  climconst3 7041  climunii 7043  climshft 7049  climres 7050  serzclim0 7054  climrecl 7055  climge0 7057  climaddlem3 7060  climmullem8 7071  climcmpc1 7083  iserzcmp0 7087  iserzex 7090  climubi 7097  climub 7098  climsup 7099  climcau 7100  caucvglem2 7102  caucvg 7107  caucvg3t 7112  serzf0 7113  ser1f0 7114  ser1clim0 7117  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  dfisum 7135  isumvalt 7136  isumclim3t 7143  isumclim5t 7145  reccnv 7161  infcvglem1 7164  expcnvlem3 7172  expcnvlem5 7174  expcnvlem6 7175  expcnv 7176  geolim 7180  geolim1 7182  cvgratlem2 7194  elcncf 7208  negfcncf 7212  rescncf 7215  mulc1cncf 7222  ivthlem1 7224  ivthlem4 7227  ivthlem6 7229  ivthlem7 7230  ivthlem8 7231  ivthlem9 7232  isupivth 7233  ivthlem4OLD 7236  ivthlem6OLD 7238  ivthlem7OLD 7239  ivthlem8OLD 7240  ivth2OLD 7242  efseq1ex 7256  efaddlem24 7311  efaddlem27 7314  eftlext 7328  ef1tlub 7332  abspef01tlub 7344  efcnlem4 7370  reefiso 7378  ruclem4 7464  ruclem32 7492  ruclem33 7493  ruclem35 7495  infxpdom 7522  fctop 7600  cctop 7602  blfval 7787  blval 7789  elbl 7790  elbl3 7792  blss 7805  metcnp2 7840  metcni 7846  metcnss 7850  metcnss2 7851  cncfmet 7857  bl2ioo 7863  lmbr 7880  iscau 7888  iscau3 7890  iscau4 7892  lmbrnns 7894  lmcvgnns 7895  lmss 7904  caussi 7905  causs 7906  lmfexlem3 7909  lmle 7911  lmclim 7914  metelcls 7916  metcnp4lem2 7919  metcnp4 7920  metcn4i 7922  xplmi 7923  xplm 7925  xpcn 7926  iscms2lem3 7941  iscms2lem4 7942  lmcau 7946  cncms 7948  bcthlem2 7950  bcthlem29 7977  isnvlem 8181  nvi 8185  nvelbl 8276  nvelbl2 8277  nvcni 8279  nvlmle 8281  nmcnilem 8285  va1cnlem 8292  sm1cnilem 8294  nvcnpi4 8368  nmofval 8370  nmosetn0 8373  nmolb 8379  nmoubi 8380  nmobndseqi 8385  bloval 8386  isblo 8387  nmo0 8396  nmlno0lem 8398  blocnilem 8408  siilem2 8456  ubthlem1 8473  ubthi 8488  minveclem9 8497  minveclem24 8512  minveclem27 8515  minveclem28 8516  minveclem39 8531  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  logltbt 8715  h2hcau 8788  h2hlm 8789  normlem7tALT 8924  norm3lemt 8958  hcau 8990  hcau2 8994  hlim 8995  hlim2 8999  hhcms 9011  hlim0 9044  hlimcaui 9045  hlimunii 9047  hhsscms 9089  occllem6 9117  projlem1 9125  projlem2 9126  projlem7 9131  projlem17 9141  projlem20 9144  projlem25 9149  projlem26 9150  projlem31 9155  pjth 9171  cmcm3t 9498  pjnormt 9609  pjnelt 9611  elcnopt 9723  elbdopt 9727  nmopsetn0 9732  nmfnsetn0 9745  elcnfnt 9749  nmoplbt 9771  nmopubt 9772  cnopct 9776  nmfnlbt 9787  nmfnleubt 9788  cnfnct 9793  0cnop 9842  0cnfn 9843  idcnop 9844  nmop0 9849  nmfn0 9850  nmlnop0ALT 9858  nmcopexlem2 9890  nmcopexlem4 9892  nmcopexlem6 9894  nmcopex 9895  lnopcont 9902  nmcfnexlem2 9919  nmcfnexlem4 9921  nmcfnexlem6 9923  nmcfnex 9924  lnfncont 9929  nlelch 9932  branmfnt 9976  leop3t 9996  hmopidmch 10017  stelt 10079  stle1t 10090  cvmdt 10200  cvdmdt 10201  cvexcht 10238  cdj3 10302  abs2sqlet 10308  abs2sqltt 10309  nndivlub 10358  mslb1 10509  msra3 10511

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409  df-op 2412  df-br 2615

Copyright terms: Public domain