MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breq1d Structured version   Unicode version

Theorem breq1d 4222
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
breq1d  |-  ( ph  ->  ( A R C  <-> 
B R C ) )

Proof of Theorem breq1d
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breq1 4215 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   class class class wbr 4212
This theorem is referenced by:  eqbrtrd  4232  syl6eqbr  4249  sbcbr2g  4264  pofun  4519  dffv2  5796  fmptco  5901  isorel  6046  soisores  6047  soisoi  6048  isocnv  6050  isotr  6056  f1owe  6073  f1oweALT  6074  weniso  6075  caovordig  6252  caovordg  6254  caovord  6258  frxp  6456  xporderlem  6457  fnwelem  6461  reldmtpos  6487  brtpos  6488  tpostpos  6499  tposoprab  6515  th3qlem2  7011  ensn1g  7172  fndmeng  7183  xpsneng  7193  xpcomco  7198  pwdom  7259  ordtypelem6  7492  ordtypelem7  7493  wdompwdom  7546  infdiffi  7612  r1sdom  7700  pm54.43  7887  prdom2  7890  indcardi  7922  alephordi  7955  cdalepw  8076  fin23lem26  8205  fin23lem23  8206  fin23lem22  8207  fin23lem27  8208  uniimadomf  8420  alephval2  8447  inar1  8650  nqereu  8806  ltrnq  8856  prlem934  8910  prlem936  8924  ltasr  8975  addgt0sr  8979  axpre-ltadd  9042  axpre-sup  9044  ltsubadd  9498  lesubadd  9500  ltaddsub2  9503  leaddsub2  9505  ltaddpos  9518  lesub2  9523  ltnegcon2  9530  lenegcon2  9533  addge01  9538  subge0  9541  suble0  9542  lesub0  9544  ltordlem  9552  mulgt1  9869  ltmulgt11  9870  gt0div  9876  ge0div  9877  ltmuldiv  9880  ltmuldiv2  9881  lemuldiv2  9890  ltrec  9891  lerec2  9898  ltdiv23  9901  lediv23  9902  addltmul  10203  avglt1  10205  avgle1  10207  avgle  10209  zlem1lt  10327  rpnnen1lem5  10604  reexALT  10606  xrmin2  10766  xltnegi  10802  xmulval  10811  xlesubadd  10842  xmullem2  10844  uzenom  11304  seqf1olem1  11362  leexp2r  11437  sqlecan  11487  expmulnbnd  11511  hashbnd  11624  hashle00  11669  hashgt12el2  11683  hashf1  11706  seqcoll  11712  shftfval  11885  shftfib  11887  shftfn  11888  2shfti  11895  shftidt2  11896  sqrlem1  12048  sqrlem2  12049  sqrlem6  12053  sqrlem7  12054  absdiflt  12121  absdifle  12122  lenegsq  12124  cau3lem  12158  limsupgle  12271  limsupgre  12275  clim  12288  rlim  12289  rlim2  12290  clim2  12298  clim0  12300  clim0c  12301  rlim0  12302  rlim0lt  12303  climi0  12306  ello1  12309  ello1mpt  12315  elo1  12320  lo1o1  12326  rlimclim1  12339  rlimclim  12340  climrlim2  12341  rlimuni  12344  climuni  12346  lo1res  12353  rlimresb  12359  rlimeq  12363  2clim  12366  climshftlem  12368  climshft  12370  climabs0  12379  o1co  12380  rlimcn1  12382  rlimcn2  12384  climcn1  12385  climcn2  12386  addcn2  12387  subcn2  12388  mulcn2  12389  o1of2  12406  o1rlimmul  12412  rlimdiv  12439  rlimno1  12447  isershft  12457  isercoll  12461  climsup  12463  climcau  12464  caucvgrlem  12466  caucvgrlem2  12468  caurcvg2  12471  caucvg  12472  caucvgb  12473  serf0  12474  iseraltlem2  12476  iseralt  12478  sumeq1f  12482  sumeq2w  12486  sumeq2ii  12487  cbvsum  12489  sumrb  12507  summolem2  12510  summo  12511  zsum  12512  o1fsum  12592  cvgcmp  12595  cvgcmpce  12597  isumshft  12619  climcndslem1  12629  geolim  12647  geolim2  12648  geoisum1c  12657  mertenslem1  12661  mertenslem2  12662  mertens  12663  sin01bnd  12786  cos01bnd  12787  rpnnen  12826  ruclem9  12837  ruclem12  12840  sadcaddlem  12969  gcddvds  13015  dvdssq  13060  isprm  13081  isprm2lem  13086  isprm6  13109  isprm5  13112  odzdvds  13181  pclem  13212  pcprecl  13213  pcprendvds  13214  pcpremul  13217  pcval  13218  pceulem  13219  pczndvds  13238  pcelnn  13243  pc2dvds  13252  pcadd  13258  pcadd2  13259  pcmpt  13261  prmpwdvds  13272  prmreclem1  13284  prmreclem5  13288  prmreclem6  13289  4sqlem17  13329  vdwlem10  13358  ramval  13376  0ram  13388  ram0  13390  ramz2  13392  ramub1lem2  13395  imasaddfnlem  13753  imasvscafn  13762  imasleval  13766  mreexexlemd  13869  oddvdsnn0  15182  oddvds  15185  odf1  15198  odf1o1  15206  odf1o2  15207  gexdvds  15218  sylow1lem3  15234  efginvrel2  15359  efgsfo  15371  efgredlemd  15376  efgredlem  15379  efgred  15380  gexexlem  15467  torsubg  15469  oddvdssubg  15470  lt6abl  15504  ablfacrplem  15623  ablfacrp  15624  ablfaclem3  15645  abvfval  15906  abvpropd  15930  znf1o  16832  znidomb  16842  cygznlem1  16847  cctop  17070  ordthmeolem  17833  csdfil  17926  ufilen  17962  ptcmplem2  18084  ptcmplem3  18085  cnextfvval  18096  prdsxmetlem  18398  blfvalps  18413  elblps  18417  elbl  18418  elbl3ps  18421  elbl3  18422  blres  18461  imasf1obl  18518  blcld  18535  comet  18543  stdbdmetval  18544  stdbdbl  18547  metcnp2  18572  txmetcnp  18577  dscopn  18621  ngptgp  18677  nlmvscn  18723  nrginvrcn  18727  nmoval  18749  nghmcn  18779  cnbl0  18808  cnblcld  18809  bl2ioo  18823  recld2  18845  icccmplem2  18854  addcnlem  18894  divcn  18898  elcncf  18919  elcncf2  18920  cncfi  18924  rescncf  18927  mulc1cncf  18935  cncfco  18937  cncfmet  18938  cnheiborlem  18979  cnheibor  18980  cnllycmp  18981  evth  18984  htpycc  19005  phtpycc  19016  pcohtpylem  19044  pcoass  19049  pcorevlem  19051  nmoleub2lem2  19124  nmoleub3  19127  nmhmcn  19128  ipcau2  19191  ipcn  19200  lmmbr2  19212  lmmcvg  19214  lmmbrf  19215  fmcfil  19225  iscau2  19230  iscau4  19232  iscauf  19233  caucfil  19236  iscmet3lem3  19243  iscmet3lem1  19244  iscmet3lem2  19245  cfilresi  19248  cfilres  19249  caussi  19250  causs  19251  lmle  19254  lmclim  19255  bcthlem1  19277  bcthlem4  19280  bcth  19282  minveclem3b  19329  minveclem3  19330  minveclem4  19333  minveclem5  19334  minveclem7  19336  pmltpclem1  19345  pmltpc  19347  ivthlem1  19348  ivthlem2  19349  ivthlem3  19350  ivth  19351  cniccbdd  19358  ovolunlem1  19393  ovoliunlem1  19398  ovoliunlem2  19399  ovoliunlem3  19400  ovolshftlem1  19405  ovolscalem1  19409  ovolicc1  19412  ovolicc2lem3  19415  ovolicc2lem4  19416  ovolicc2lem5  19417  ioombl1lem4  19455  ioombl1  19456  uniioombllem6  19480  volsup2  19497  volcn  19498  mbfmulc2lem  19539  mbfsup  19556  mbflimsup  19558  itg1climres  19606  mbfi1fseqlem6  19612  mbfi1fseq  19613  mbfi1flimlem  19614  itg2leub  19626  itg2seq  19634  itg2mulclem  19638  itg2monolem1  19642  itg2mono  19645  itg2i1fseq  19647  itg2addlem  19650  itg2gt0  19652  itg2cnlem1  19653  itg2cnlem2  19654  itg2cn  19655  bddmulibl  19730  itgcn  19734  ellimc3  19766  dveflem  19863  dvferm1lem  19868  dvferm2lem  19870  rolle  19874  dvlip  19877  dvlipcn  19878  dvlip2  19879  c1liplem1  19880  c1lip3  19883  dvge0  19890  dvivthlem1  19892  lhop1lem  19897  lhop1  19898  dvcvx  19904  dvfsumabs  19907  dvfsumlem2  19911  dvfsumrlim  19915  ftc1a  19921  ftc1lem4  19923  ftc1lem6  19925  itgsubstlem  19932  mdegleb  19987  mdegmullem  20001  deg1lt0  20014  ply1divmo  20058  ply1divex  20059  ply1divalg2  20061  q1peqb  20077  fta1g  20090  dgrub  20153  coe1termlem  20176  dgrcolem2  20192  dgrco  20193  quotval  20209  plydivlem3  20212  plydivlem4  20213  plydivex  20214  plydivalg  20216  quotlem  20217  plyrem  20222  fta1  20225  aannenlem1  20245  aannenlem2  20246  aalioulem3  20251  aalioulem4  20252  aalioulem5  20253  aalioulem6  20254  aaliou  20255  aaliou2  20257  aaliou2b  20258  ulmval  20296  ulm2  20301  ulmclm  20303  ulmshftlem  20305  ulmcaulem  20310  ulmcau  20311  ulmss  20313  ulmcn  20315  ulmdvlem1  20316  ulmdvlem3  20318  mtestbdd  20321  iblulm  20323  itgulm  20324  radcnvlem1  20329  pserulm  20338  abelthlem2  20348  abelthlem5  20351  abelthlem7  20354  abelthlem8  20355  abelthlem9  20356  abelth  20357  pilem3  20369  sincosq2sgn  20407  sincosq3sgn  20408  sincosq4sgn  20409  logltb  20494  logcnlem5  20537  cxpcn3lem  20631  cxpcn3  20632  cxpaddle  20636  logreclem  20660  rlimcnp  20804  rlimcnp2  20805  xrlimcnp  20807  rlimcxp  20812  cxploglim  20816  jensen  20827  emcllem6  20839  emcllem7  20840  ftalem2  20856  ftalem3  20857  ftalem5  20859  sqfpc  20920  mumullem2  20963  sqff1o  20965  chtublem  20995  chtub  20996  fsumvma2  20998  chpchtsum  21003  logexprlim  21009  bposlem6  21073  lgslem2  21081  lgslem3  21082  lgsval  21084  lgsfcl2  21086  lgsfle1  21089  lgsle1  21095  lgsdirprm  21113  chtppilimlem2  21168  chtppilim  21169  dchrisumlema  21182  dchrisumlem1  21183  dchrisumlem2  21184  dchrisumlem3  21185  dchrisum  21186  dchrmusumlema  21187  dchrvmasumlem2  21192  dchrisum0flblem1  21202  dchrisum0lema  21208  2vmadivsumlem  21234  chpdifbndlem1  21247  selberg3lem1  21251  selberg4lem1  21254  pntrsumbnd  21260  pntrsumbnd2  21261  selbergsb  21269  pntrlog2bndlem3  21273  pntrlog2bndlem5  21275  pntrlog2bndlem6  21277  pntpbnd1  21280  pntpbnd2  21281  pntibndlem2  21285  pntibndlem3  21286  pntibnd  21287  pntlemn  21294  pntlemj  21297  pntlemi  21298  pntlemo  21301  pntlem3  21303  pntlemp  21304  pntleml  21305  pnt3  21306  padicabv  21324  ostth2lem2  21328  ostth3  21332  ostth  21333  umgrale  21356  umgrafi  21357  umgra1  21361  uslgra1  21392  1pthoncl  21592  2pthoncl  21603  umgrabi  21705  isnvlem  22089  nvelbl  22185  nvelbl2  22186  nmoofval  22263  nmosetn0  22266  nmoolb  22272  nmoubi  22273  nmounbseqi  22278  nmounbseqiOLD  22279  nmobndseqi  22280  nmobndseqiOLD  22281  bloval  22282  isblo  22283  nmoo0  22292  nmlno0lem  22294  blocnilem  22305  siilem2  22353  ubthlem1  22372  ubthlem2  22373  ubthlem3  22374  ubth  22375  minvecolem3  22378  minvecolem4  22382  minvecolem5  22383  minvecolem7  22385  htthlem  22420  htth  22421  h2hcau  22482  h2hlm  22483  normlem7tALT  22621  norm3lemt  22654  hcau  22686  hlimi  22690  hlim2  22694  cmcm3  23117  pjnorm  23226  pjnel  23228  elcnop  23360  elbdop  23363  nmopsetn0  23368  nmfnsetn0  23381  elcnfn  23385  hhcno  23407  hhcnf  23408  nmoplb  23410  nmopub  23411  cnopc  23416  nmfnlb  23427  nmfnleub  23428  cnfnc  23433  idcnop  23484  nmop0  23489  nmfn0  23490  nmlnop0iALT  23498  nmcexi  23529  nmcopexi  23530  lnconi  23536  lnopcon  23538  nmcfnexi  23554  lnfncon  23559  branmfn  23608  leop3  23628  opsqrlem6  23648  cvmd  23839  cvdmd  23840  cvexch  23877  cdj3i  23944  fmptcof2  24076  xraddge02  24123  xdivpnfrp  24179  isofld  24235  ofldadd  24238  ofldmul  24239  sqsscirc2  24307  cnre2csqlem  24308  xrge0iifiso  24321  lmdvg  24338  qqhcn  24375  qqhucn  24376  brfae  24599  dya2ub  24620  ballotlemfc0  24750  ballotlemfcc  24751  ballotlemimin  24763  ballotlemic  24764  ballotlemsv  24767  ballotlemfrcn0  24787  ballotlemrc  24788  lgamgulmlem2  24814  lgamgulmlem3  24815  lgamgulmlem5  24817  lgamgulmlem6  24818  lgambdd  24821  lgamucov  24822  lgamcvglem  24824  erdszelem8  24884  kur14  24902  snmlval  25018  snmlflim  25019  sinccvg  25110  abs2sqle  25120  abs2sqlt  25121  ntrivcvg  25225  ntrivcvgn0  25226  ntrivcvgmullem  25229  prodeq1f  25234  prodeq2w  25238  prodeq2ii  25239  prodrblem2  25257  prodmolem2  25261  prodmo  25262  zprod  25263  fprodntriv  25268  faclim2  25367  poseq  25528  soseq  25529  sltval  25602  brimg  25782  brbtwn2  25844  colinearalg  25849  axcontlem10  25912  cgrtriv  25936  cgrdegen  25938  brofs  25939  cgrextend  25942  segconeu  25945  fvtransport  25966  transportprops  25968  brifs  25977  ifscgr  25978  brcgr3  25980  cgrxfr  25989  brfs  26013  btwnconn1lem7  26027  btwnconn1lem11  26031  btwnconn1lem12  26032  btwnconn1lem14  26034  brsegle  26042  segleantisym  26049  outsideofeu  26065  nndivlub  26208  itg2addnclem  26256  itg2addnclem3  26258  itg2addnc  26259  itg2gt0cn  26260  bddiblnc  26275  ftc1cnnclem  26278  ftc1cnnc  26279  ftc1anclem5  26284  ftc1anclem6  26285  ftc1anc  26288  areacirclem1  26292  areacirclem2  26293  areacirclem4  26295  areacirclem5  26296  areacirc  26297  nn0prpwlem  26325  nn0prpw  26326  seqpo  26451  incsequz2  26453  lmclim2  26464  geomcau  26465  caushft  26467  prdsbnd  26502  ismtyima  26512  heiborlem4  26523  heiborlem6  26525  heiborlem7  26526  bfplem1  26531  bfplem2  26532  rrndstprj2  26540  rrncmslem  26541  rrnequiv  26544  irrapxlem3  26887  irrapxlem4  26888  irrapxlem5  26889  irrapxlem6  26890  pellexlem3  26894  monotoddzz  27006  jm2.19  27064  rmydioph  27085  fnwe2lem2  27126  islinds  27256  lindsss  27271  hbtlem1  27304  hbtlem2  27305  hbtlem7  27306  hbtlem4  27307  hbtlem5  27309  hbtlem6  27310  dgrsub2  27316  symggen  27388  fiuneneq  27490  evth2f  27662  evthf  27674  cncmpmax  27679  rfcnpre4  27681  fmul01  27686  climinf  27708  climsuse  27710  stoweidlem7  27732  stoweidlem9  27734  stoweidlem15  27740  stoweidlem16  27741  stoweidlem18  27743  stoweidlem21  27746  stoweidlem26  27751  stoweidlem31  27756  stoweidlem34  27759  stoweidlem36  27761  stoweidlem37  27762  stoweidlem41  27766  stoweidlem44  27769  stoweidlem45  27770  stoweidlem46  27771  stoweidlem48  27773  stoweidlem51  27776  stoweidlem52  27777  stoweidlem55  27780  stoweidlem59  27784  stoweidlem60  27785  ubmelm1fzo  28127  swrdccatin2  28210  prmgt1  28223  2cshw1lem3  28250  2cshwcom  28267  cshweqdif2  28270  frgrawopreglem2  28434  oposlem  29981  opltcon2b  30004  pats  30083  ishlat1  30150  cvrexch  30217  atle  30233  athgt  30253  1cvrco  30269  3atlem5  30284  4atlem3  30393  dalawlem15  30682  lhprelat3N  30837  lautle  30881  lautcvr  30889  ltrnatb  30934  ltrneq2  30945  cdlemefr32sn2aw  31201  cdlemefs32sn1aw  31211  cdleme32fvaw  31236  cdleme35sn3a  31256  cdleme46frvlpq  31301  cdleme48gfv  31334  trlord  31366  cdlemg1fvawlemN  31370  cdlemg7fvbwN  31404  cdlemg31d  31497  istendo  31557  dva1dim  31782  dvhb1dimN  31783  diafval  31829  diaelval  31831  cdlemm10N  31916  dihopelvalcpre  32046  dihmeetcN  32100  dihmeetlem6  32107  dihjatc1  32109
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator