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

Theorem breq1d 4290
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 4283 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362   class class class wbr 4280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281
This theorem is referenced by:  eqbrtrd  4300  syl6eqbr  4317  sbcbr2g  4336  pofun  4644  dffv2  5752  fmptco  5863  isorel  6004  soisores  6005  soisoi  6006  isocnv  6008  isotr  6014  f1owe  6031  weniso  6032  caovordig  6257  caovordg  6259  caovord  6263  f1oweALT  6550  frxp  6671  xporderlem  6672  fnwelem  6676  reldmtpos  6742  brtpos  6743  tpostpos  6754  tposoprab  6770  th3qlem2  7195  ensn1g  7362  fndmeng  7374  xpsneng  7384  xpcomco  7389  pwdom  7451  ordtypelem6  7725  ordtypelem7  7726  wdompwdom  7781  infdiffi  7851  r1sdom  7969  pm54.43  8158  prdom2  8161  indcardi  8199  alephordi  8232  cdalepw  8353  fin23lem26  8482  fin23lem23  8483  fin23lem22  8484  fin23lem27  8485  uniimadomf  8697  alephval2  8724  inar1  8930  nqereu  9086  ltrnq  9136  prlem934  9190  prlem936  9204  ltasr  9255  addgt0sr  9259  axpre-ltadd  9322  axpre-sup  9324  ltsubadd  9797  lesubadd  9799  ltaddsub2  9802  leaddsub2  9804  ltaddpos  9817  lesub2  9822  ltnegcon2  9829  lenegcon2  9832  addge01  9837  subge0  9840  suble0  9841  lesub0  9844  ltordlem  9853  mulgt1  10176  ltmulgt11  10177  gt0div  10183  ge0div  10184  ltmuldiv  10190  ltmuldiv2  10191  lemuldiv2  10200  ltrec  10201  lerec2  10208  ltdiv23  10211  lediv23  10212  addltmul  10548  avglt1  10550  avgle1  10552  avgle  10554  zlem1lt  10684  zgt0ge1  10686  rpnnen1lem5  10971  reexALT  10973  xrmin2  11138  xltnegi  11174  xmulval  11183  xlesubadd  11214  xmullem2  11216  dfceil2  11664  uzenom  11771  seqf1olem1  11829  leexp2r  11905  sqlecan  11956  expmulnbnd  11980  hashbnd  12093  hashle00  12142  hashgt12el2  12158  hashge3el3dif  12171  hashf1  12194  seqcoll  12200  lswccatn0lsw  12271  swrdccatin2  12362  swrd2lsw  12536  2swrd2eqwrdeq  12537  shftfval  12543  shftfib  12545  shftfn  12546  2shfti  12553  shftidt2  12554  sqrlem1  12716  sqrlem2  12717  sqrlem6  12721  sqrlem7  12722  absdiflt  12789  absdifle  12790  lenegsq  12792  cau3lem  12826  limsupgle  12939  limsupgre  12943  clim  12956  rlim  12957  rlim2  12958  clim2  12966  clim0  12968  clim0c  12969  rlim0  12970  rlim0lt  12971  climi0  12974  ello1  12977  ello1mpt  12983  elo1  12988  lo1o1  12994  rlimclim1  13007  rlimclim  13008  climrlim2  13009  rlimuni  13012  climuni  13014  lo1res  13021  rlimresb  13027  rlimeq  13031  2clim  13034  climshftlem  13036  climshft  13038  climabs0  13047  o1co  13048  rlimcn1  13050  rlimcn2  13052  climcn1  13053  climcn2  13054  addcn2  13055  subcn2  13056  mulcn2  13057  o1of2  13074  o1rlimmul  13080  rlimdiv  13107  rlimno1  13115  isershft  13125  isercoll  13129  climsup  13131  climcau  13132  caucvgrlem  13134  caucvgrlem2  13136  caurcvg2  13139  caucvg  13140  caucvgb  13141  serf0  13142  iseraltlem2  13144  iseralt  13146  sumeq1  13150  sumeq2w  13153  sumeq2ii  13154  sumrb  13174  summolem2  13177  summo  13178  zsum  13179  o1fsum  13259  cvgcmp  13262  cvgcmpce  13264  isumshft  13285  climcndslem1  13295  geolim  13313  geolim2  13314  geoisum1c  13323  mertenslem1  13327  mertenslem2  13328  mertens  13329  sin01bnd  13452  cos01bnd  13453  rpnnen  13492  ruclem9  13503  ruclem12  13506  sadcaddlem  13636  gcddvds  13682  dvdssq  13727  isprm  13748  isprm2lem  13753  prmgt1  13765  isprm6  13778  isprm5  13781  odzdvds  13850  pclem  13888  pcprecl  13889  pcprendvds  13890  pcpremul  13893  pcval  13894  pceulem  13895  pczndvds  13914  pcelnn  13919  pc2dvds  13928  pcadd  13934  pcadd2  13935  pcmpt  13937  prmpwdvds  13948  prmreclem1  13960  prmreclem5  13964  prmreclem6  13965  4sqlem17  14005  vdwlem10  14034  ramval  14052  0ram  14064  ram0  14066  ramz2  14068  ramub1lem2  14071  imasaddfnlem  14449  imasvscafn  14458  imasleval  14462  mreexexlemd  14565  symggen  15956  oddvdsnn0  16027  oddvds  16030  odf1  16043  odf1o1  16051  odf1o2  16052  gexdvds  16063  sylow1lem3  16079  efginvrel2  16204  efgsfo  16216  efgredlemd  16221  efgredlem  16224  efgred  16225  gexexlem  16314  torsubg  16316  oddvdssubg  16317  lt6abl  16351  ablfacrplem  16540  ablfacrp  16541  ablfaclem3  16562  abvfval  16827  abvpropd  16851  evlslem2  17525  znf1o  17826  znidomb  17836  cygznlem1  17841  frlmup1  18068  islinds  18080  lindsss  18095  cctop  18452  ordthmeolem  19216  csdfil  19309  ufilen  19345  ptcmplem2  19467  ptcmplem3  19468  cnextfvval  19479  prdsxmetlem  19785  blfvalps  19800  elblps  19804  elbl  19805  elbl3ps  19808  elbl3  19809  blres  19848  imasf1obl  19905  blcld  19922  comet  19930  stdbdmetval  19931  stdbdbl  19934  metcnp2  19959  txmetcnp  19964  dscopn  20008  ngptgp  20064  nlmvscn  20110  nrginvrcn  20114  nmoval  20136  nghmcn  20166  cnbl0  20195  cnblcld  20196  bl2ioo  20211  recld2  20233  icccmplem2  20242  addcnlem  20282  divcn  20286  elcncf  20307  elcncf2  20308  cncfi  20312  rescncf  20315  mulc1cncf  20323  cncfco  20325  cncfmet  20326  cnheiborlem  20368  cnheibor  20369  cnllycmp  20370  evth  20373  htpycc  20394  phtpycc  20405  pcohtpylem  20433  pcoass  20438  pcorevlem  20440  nmoleub2lem2  20513  nmoleub3  20516  nmhmcn  20517  ipcau2  20591  ipcn  20600  lmmbr2  20612  lmmcvg  20614  lmmbrf  20615  fmcfil  20625  iscau2  20630  iscau4  20632  iscauf  20633  caucfil  20636  iscmet3lem3  20643  iscmet3lem1  20644  iscmet3lem2  20645  cfilresi  20648  cfilres  20649  caussi  20650  causs  20651  lmle  20654  lmclim  20655  bcthlem1  20677  bcthlem4  20680  bcth  20682  minveclem3b  20757  minveclem3  20758  minveclem4  20761  minveclem5  20762  minveclem7  20764  pmltpclem1  20774  pmltpc  20776  ivthlem1  20777  ivthlem2  20778  ivthlem3  20779  ivth  20780  cniccbdd  20787  ovolunlem1  20822  ovoliunlem1  20827  ovoliunlem2  20828  ovoliunlem3  20829  ovolshftlem1  20834  ovolscalem1  20838  ovolicc1  20841  ovolicc2lem3  20844  ovolicc2lem4  20845  ovolicc2lem5  20846  ioombl1lem4  20884  ioombl1  20885  uniioombllem6  20910  volsup2  20927  volcn  20928  mbfmulc2lem  20967  mbfsup  20984  mbflimsup  20986  itg1climres  21034  mbfi1fseqlem6  21040  mbfi1fseq  21041  mbfi1flimlem  21042  itg2leub  21054  itg2seq  21062  itg2mulclem  21066  itg2monolem1  21070  itg2mono  21073  itg2i1fseq  21075  itg2addlem  21078  itg2gt0  21080  itg2cnlem1  21081  itg2cnlem2  21082  itg2cn  21083  bddmulibl  21158  itgcn  21162  ellimc3  21196  dveflem  21293  dvferm1lem  21298  dvferm2lem  21300  rolle  21304  dvlip  21307  dvlipcn  21308  dvlip2  21309  c1liplem1  21310  c1lip3  21313  dvge0  21320  dvivthlem1  21322  lhop1lem  21327  lhop1  21328  dvcvx  21334  dvfsumabs  21337  dvfsumlem2  21341  dvfsumrlim  21345  ftc1a  21351  ftc1lem4  21353  ftc1lem6  21355  itgsubstlem  21362  mdegleb  21420  mdegmullem  21434  deg1lt0  21447  ply1divmo  21492  ply1divex  21493  ply1divalg2  21495  q1peqb  21511  fta1g  21524  dgrub  21587  coe1termlem  21610  dgrcolem2  21626  dgrco  21627  quotval  21643  plydivlem3  21646  plydivlem4  21647  plydivex  21648  plydivalg  21650  quotlem  21651  plyrem  21656  fta1  21659  aannenlem1  21679  aannenlem2  21680  aalioulem3  21685  aalioulem4  21686  aalioulem5  21687  aalioulem6  21688  aaliou  21689  aaliou2  21691  aaliou2b  21692  ulmval  21730  ulm2  21735  ulmclm  21737  ulmshftlem  21739  ulmcaulem  21744  ulmcau  21745  ulmss  21747  ulmcn  21749  ulmdvlem1  21750  ulmdvlem3  21752  mtestbdd  21755  iblulm  21757  itgulm  21758  radcnvlem1  21763  pserulm  21772  abelthlem2  21782  abelthlem5  21785  abelthlem7  21788  abelthlem8  21789  abelthlem9  21790  abelth  21791  pilem3  21803  sincosq2sgn  21846  sincosq3sgn  21847  sincosq4sgn  21848  logltb  21933  logcnlem5  21976  cxpcn3lem  22070  cxpcn3  22071  cxpaddle  22075  logreclem  22099  rlimcnp  22244  rlimcnp2  22245  xrlimcnp  22247  rlimcxp  22252  cxploglim  22256  jensen  22267  emcllem6  22279  emcllem7  22280  ftalem2  22296  ftalem3  22297  ftalem5  22299  sqfpc  22360  mumullem2  22403  sqff1o  22405  chtublem  22435  chtub  22436  fsumvma2  22438  chpchtsum  22443  logexprlim  22449  bposlem6  22513  lgslem2  22521  lgslem3  22522  lgsval  22524  lgsfcl2  22526  lgsfle1  22529  lgsle1  22535  lgsdirprm  22553  chtppilimlem2  22608  chtppilim  22609  dchrisumlema  22622  dchrisumlem1  22623  dchrisumlem2  22624  dchrisumlem3  22625  dchrisum  22626  dchrmusumlema  22627  dchrvmasumlem2  22632  dchrisum0flblem1  22642  dchrisum0lema  22648  2vmadivsumlem  22674  chpdifbndlem1  22687  selberg3lem1  22691  selberg4lem1  22694  pntrsumbnd  22700  pntrsumbnd2  22701  selbergsb  22709  pntrlog2bndlem3  22713  pntrlog2bndlem5  22715  pntrlog2bndlem6  22717  pntpbnd1  22720  pntpbnd2  22721  pntibndlem2  22725  pntibndlem3  22726  pntibnd  22727  pntlemn  22734  pntlemj  22737  pntlemi  22738  pntlemo  22741  pntlem3  22743  pntlemp  22744  pntleml  22745  pnt3  22746  padicabv  22764  ostth2lem2  22768  ostth3  22772  ostth  22773  brbtwn2  22974  colinearalg  22979  axcontlem10  23042  umgrale  23078  umgrafi  23079  umgra1  23083  uslgra1  23114  1pthoncl  23314  2pthoncl  23325  umgrabi  23427  isnvlem  23811  nvelbl  23907  nvelbl2  23908  nmoofval  23985  nmosetn0  23988  nmoolb  23994  nmoubi  23995  nmounbseqi  24000  nmounbseqiOLD  24001  nmobndseqi  24002  nmobndseqiOLD  24003  bloval  24004  isblo  24005  nmoo0  24014  nmlno0lem  24016  blocnilem  24027  siilem2  24075  ubthlem1  24094  ubthlem2  24095  ubthlem3  24096  ubth  24097  minvecolem3  24100  minvecolem4  24104  minvecolem5  24105  minvecolem7  24107  htthlem  24142  htth  24143  h2hcau  24204  h2hlm  24205  normlem7tALT  24344  norm3lemt  24377  hcau  24409  hlimi  24413  hlim2  24417  cmcm3  24841  pjnorm  24950  pjnel  24952  elcnop  25084  elbdop  25087  nmopsetn0  25092  nmfnsetn0  25105  elcnfn  25109  hhcno  25131  hhcnf  25132  nmoplb  25134  nmopub  25135  cnopc  25140  nmfnlb  25151  nmfnleub  25152  cnfnc  25157  idcnop  25208  nmop0  25213  nmfn0  25214  nmlnop0iALT  25222  nmcexi  25253  nmcopexi  25254  lnconi  25260  lnopcon  25262  nmcfnexi  25278  lnfncon  25283  branmfn  25332  leop3  25352  opsqrlem6  25372  cvmd  25563  cvdmd  25564  cvexch  25601  cdj3i  25668  fmptcof2  25803  xraddge02  25875  xdivpnfrp  25931  omndadd  25993  omndmul  26001  archirngz  26030  archiabllem2a  26035  isorng  26120  sqsscirc2  26193  cnre2csqlem  26194  xrge0iifiso  26219  lmdvg  26237  qqhcn  26274  qqhucn  26275  brfae  26518  dya2ub  26539  oddpwdc  26585  eulerpartlemd  26597  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemimin  26736  ballotlemic  26737  ballotlemsv  26740  ballotlemfrcn0  26760  ballotlemrc  26761  sgnmul  26773  sgnmulsgn  26780  signsplypnf  26799  signsply0  26800  signswch  26810  signsvfn  26831  signsvfnn  26835  signlem0  26836  lgamgulmlem2  26864  lgamgulmlem3  26865  lgamgulmlem5  26867  lgamgulmlem6  26868  lgambdd  26871  lgamucov  26872  lgamcvglem  26874  erdszelem8  26934  kur14  26952  snmlval  27068  snmlflim  27069  sinccvg  27165  abs2sqle  27172  abs2sqlt  27173  ntrivcvg  27259  ntrivcvgn0  27260  ntrivcvgmullem  27263  prodeq1f  27268  prodeq2w  27272  prodeq2ii  27273  prodrblem2  27291  prodmolem2  27295  prodmo  27296  zprod  27297  fprodntriv  27302  faclim2  27401  poseq  27561  soseq  27562  sltval  27635  brimg  27815  cgrtriv  27880  cgrdegen  27882  brofs  27883  cgrextend  27886  segconeu  27889  fvtransport  27910  transportprops  27912  brifs  27921  ifscgr  27922  brcgr3  27924  cgrxfr  27933  brfs  27957  btwnconn1lem7  27971  btwnconn1lem11  27975  btwnconn1lem12  27976  btwnconn1lem14  27978  brsegle  27986  segleantisym  27993  outsideofeu  28009  nndivlub  28152  heicant  28270  dvtanlem  28285  itg2addnclem  28287  itg2addnclem3  28289  itg2addnc  28290  itg2gt0cn  28291  bddiblnc  28306  ftc1cnnclem  28309  ftc1cnnc  28310  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anc  28319  areacirclem1  28328  areacirclem2  28329  areacirclem4  28331  areacirclem5  28332  areacirc  28333  nn0prpwlem  28361  nn0prpw  28362  seqpo  28487  incsequz2  28489  lmclim2  28498  geomcau  28499  caushft  28501  prdsbnd  28536  ismtyima  28546  heiborlem4  28557  heiborlem6  28559  heiborlem7  28560  bfplem1  28565  bfplem2  28566  rrndstprj2  28574  rrncmslem  28575  rrnequiv  28578  irrapxlem3  29010  irrapxlem4  29011  irrapxlem5  29012  irrapxlem6  29013  pellexlem3  29017  monotoddzz  29129  jm2.19  29187  rmydioph  29208  fnwe2lem2  29249  hbtlem1  29324  hbtlem2  29325  hbtlem7  29326  hbtlem4  29327  hbtlem5  29329  hbtlem6  29330  dgrsub2  29336  fiuneneq  29407  evth2f  29582  evthf  29594  cncmpmax  29599  rfcnpre4  29601  fmul01  29606  climinf  29625  climsuse  29627  stoweidlem7  29648  stoweidlem9  29650  stoweidlem15  29656  stoweidlem16  29657  stoweidlem18  29659  stoweidlem21  29662  stoweidlem26  29667  stoweidlem31  29672  stoweidlem34  29675  stoweidlem36  29677  stoweidlem37  29678  stoweidlem41  29682  stoweidlem44  29685  stoweidlem45  29686  stoweidlem46  29687  stoweidlem48  29689  stoweidlem51  29692  stoweidlem52  29693  stoweidlem55  29696  stoweidlem59  29700  stoweidlem60  29701  prmn2uzge3  30095  clwlkisclwwlk2  30298  0eusgraiff0rgra  30398  frgrawopreglem2  30484  snnen2o  30582  pgrpgt2nabel  30600  oposlem  32400  opltcon2b  32424  pats  32503  ishlat1  32570  cvrexch  32637  atle  32653  athgt  32673  1cvrco  32689  3atlem5  32704  4atlem3  32813  dalawlem15  33102  lhprelat3N  33257  lautle  33301  lautcvr  33309  ltrnatb  33354  ltrneq2  33365  cdlemefr32sn2aw  33621  cdlemefs32sn1aw  33631  cdleme32fvaw  33656  cdleme35sn3a  33676  cdleme46frvlpq  33721  cdleme48gfv  33754  trlord  33786  cdlemg1fvawlemN  33790  cdlemg7fvbwN  33824  cdlemg31d  33917  istendo  33977  dva1dim  34202  dvhb1dimN  34203  diafval  34249  diaelval  34251  cdlemm10N  34336  dihopelvalcpre  34466  dihmeetcN  34520  dihmeetlem6  34527  dihjatc1  34529
  Copyright terms: Public domain W3C validator