Theorem breq1d 3168

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

Syntax hints:   -> wi 3   <-> wb 162   = wceq 1136   class class class wbr 3158

This theorem is referenced by:  breq12dOLD 3172  eqbrtrd 3177  syl6eqbr 3194  sbcbr2g 3212  dffv2 4545  isorel 4682  isocnv 4684  isotr 4685  isotrALT 4686  f1owe 4693  f1oweALT 4694  caoprord 4800  fparlem1 4892  fparlem2 4893  th3qlem2 5185  ensn1g 5295  xpsneng 5306  xpdom2 5312  pwen 5407  pm54.43 5472  suppr 5490  infenomsub 5685  uniimadomf 5769  iundom 5770  alephordi 5818  alephval2 5846  cdaeng 5870  nnaun 5885  ltapq 6024  ltmpq 6025  prlem936a 6101  prlem936 6103  ltasr 6157  addgt0sr 6161  pre-axltadd 6238  ltadd1 6602  leadd1 6604  ltsubadd 6606  lesubadd 6608  ltaddsub2 6611  leaddsub2 6613  lt2add 6623  le2add 6624  ltaddpos 6635  ltneg 6640  leneg 6642  lenegcon2 6644  addge01 6657  ltmuldivi 6798  ltmul1 6803  mulgt1 6822  ltmulgt11 6823  ltdiv1 6826  ltdiv1OLD 6827  gt0div 6830  ge0div 6831  ltmuldiv 6840  ltmuldivOLD 6841  ltmuldiv2 6842  ltmuldiv2OLD 6843  lemuldiv2 6854  lemuldiv2OLD 6855  ltreci 6857  lt2msqi 6859  ltrec 6862  lerec 6863  lt2msq 6864  lerec2 6867  ltdiv23 6870  lediv23 6871  le2msq 6881  xrmin2 6890  nnleltp1 6933  addltmul 7024  avgle 7026  nn0ltp1le 7131  zltp1le 7185  zlem1lt 7187  fllelt 7262  fsequb 7497  seqzfval 7575  exple1 7647  sqlecan 7682  discrlem2 7702  discrlem3 7703  sqr0 7717  sqrlem4 7721  sqrlem6 7723  sqrlem12 7729  sqrlem22 7739  sqrlem24 7741  sqrgt0ii 7742  sqrlem26 7743  sqrle 7758  sqr2irr 7774  abslt 7927  absle 7928  abssubne0 7929  absdiflt 7930  absdifle 7931  lenegsq 7932  abs3lem 7954  seq1bndi 7957  seq1ublem 7958  cau2i 7960  clim 8032  sumeq2 8040  serzcmp0 8110  clm0i 8138  clmnnsi 8139  clm0nnsi 8140  clm0ii 8144  climfnn 8147  climconsti 8149  climconst3 8151  climunii 8153  climshfti 8159  climresi 8160  serzclim0 8164  climrecl 8165  climge0 8167  climabs0i 8168  climaddlem3 8171  climmullem8 8182  climcmpc1 8194  iserzcmp0 8198  iserzexi 8201  climubii 8208  climubi 8209  climsupi 8210  climcaui 8211  caucvglem2 8213  caucvgi 8218  caucvg3 8223  serzf0i 8224  ser1clim0 8228  cvgcmp3cetlem1 8244  cvgcmp3cetlem2 8245  dfisum 8247  isumval 8248  isumclim3 8256  isumclim5 8258  reccnv 8274  infcvglem1 8277  expcnvlem3 8285  expcnvlem5 8287  expcnvlem6 8288  expcnv 8289  geolim 8294  geolim1 8296  cvgratlem2 8308  elcncf 8322  negfcncfi 8326  rescncf 8329  mulc1cncf 8336  ivthlem1 8338  ivthlem4 8341  ivthlem6 8343  ivthlem7 8344  ivthlem8 8345  ivthlem9 8346  isupivthi 8347  efseq1ex 8363  efaddlem24 8418  efaddlem27 8421  eftlex 8435  ef1tlubi 8439  abspef01tlubi 8455  efcnlem4 8482  reefiso 8488  ruclem4 8577  ruclem32 8605  ruclem33 8606  ruclem35 8608  infxpdom 8635  cctop 8717  blfval 8907  blval 8909  elbl 8910  elbl3 8912  blss 8925  metcnp2 8961  metcni 8967  metcnss 8971  metcnss2 8972  cncfmet 8978  bl2ioo 8984  lmbr 9001  iscau 9009  iscau3 9011  iscau4 9013  lmbrnns 9015  lmcvgnns 9016  iscaunns 9017  lmss 9026  caussi 9027  causs 9028  lmfexlem3 9031  lmle 9033  lmclim 9036  metelcls 9038  metcnp4lem2 9042  metcnp4 9043  metcn4i 9045  xplmi 9046  xplm 9048  xpcn 9049  iscms2lem3 9064  iscms2lem4 9065  lmcau 9069  cncms 9071  bcthlem2 9073  bcthlem29 9100  isnvlem 9356  nvi 9360  nvelbl 9452  nvelbl2 9453  nvcni 9456  nvcni2 9457  nvcni3 9458  nvlmle 9460  vacnlem3 9464  nmcnilem 9471  va1cnlem 9479  sm1cnilem 9481  nvcnpi3 9556  nvcnpi4 9557  nmofval 9559  nmosetn0 9562  nmolb 9568  nmoubi 9569  nmounbseqi 9574  nmobndseqi 9575  bloval 9576  isblo 9577  nmo0 9586  nmlno0lem 9588  blocnilem 9599  siilem2 9648  ubthlem1 9667  ubthi 9684  minveclem9 9693  minveclem24 9708  minveclem27 9711  minveclem28 9712  minveclem39 9727  sincosq2sgn 9849  sincosq3sgn 9850  sincosq4sgn 9851  logltb 9925  dif1enOLD 9967  dif1card 9969  h2hcau 10273  h2hlm 10274  normlem7tALT 10410  norm3lemt 10444  hcau 10476  hcau2 10480  hlimi 10481  hlim2 10485  hhcms 10497  hlim0 10530  hlimcauii 10531  hlimuniii 10533  hhsscms 10575  occllem6 10603  projlem1 10611  projlem2 10612  projlem7 10617  projlem17 10627  projlem20 10630  projlem25 10635  projlem26 10636  projlem31 10641  pjthi 10658  cmcm3 10983  pjnorm 11096  pjnel 11098  elcnop 11212  elbdop 11216  nmopsetn0 11221  nmfnsetn0 11234  elcnfn 11238  nmoplb 11260  nmopub 11261  cnopc 11266  nmfnlb 11277  nmfnleub 11278  cnfnc 11283  0cnop 11332  0cnfn 11333  idcnop 11334  nmop0 11339  nmfn0 11340  nmlnop0iALT 11349  nmcopexlem2 11381  nmcopexlem4 11383  nmcopexlem6 11385  nmcopexi 11386  lnopcon 11393  nmcfnexlem2 11410  nmcfnexlem4 11412  nmcfnexlem6 11414  nmcfnexi 11415  lnfncon 11420  nlelchi 11423  branmfn 11467  branmfnOLD 11468  leop3 11488  opsqrlem6 11508  hmopidmchi 11515  stel 11578  stle1 11589  cvmd 11700  cvdmd 11701  cvexch 11738  cdj3i 11805  fndmeng 13390  abs2sqle 13416  abs2sqlt 13417  gcddvds 13514  isprm 13560  isprm2lem 13566  xporderlem 13740  frxp 13743  poseq 13746  soseq 13747  sltval 13780  nndivlub 13989  unpam2 14154  cntrsetlem 14709  mslb1 14717  msra3 14719  fictb 15053  infenomsubOLD 15080  fnejoin2 15213  ufilen 15261  xpeng 15373  supubt 15445  pofun 15454  seqpo 15496  incsequz2 15498  fsumltisumi 15505  fsumltisum 15506  fsumleisumi 15508  fsumleisum 15509  iserzshft2 15511  fsumlt1 15513  blssp 15526  geomcau 15531  lmclim2 15532  caushft 15533  caures 15534  addccncf 15565  sub1cncf 15567  sub2cncf 15568  txmet 15607  ismtyhmeolem 15632  heiborlem16 15652  heiborlem18 15654  heiborlem34 15670  heiborlem35 15671  heiborlem36 15672  bfplem11 15690  rrndstprj2 15700  rrncms 15701  lubprop 16563  glbprop 16568  oposlem 16668  opltcon2b 16685  patoms 16749  ishlat 16765  cvrexch 16798

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-ex 1165  df-sb 1374  df-clab 1709  df-cleq 1714  df-clel 1717  df-v 2127  df-un 2433  df-sn 2873  df-pr 2874  df-op 2877  df-br 3159

Copyright terms: Public domain