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

Theorem eqbrtrd 4045
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
Hypotheses
Ref Expression
eqbrtrd.1  |-  ( ph  ->  A  =  B )
eqbrtrd.2  |-  ( ph  ->  B R C )
Assertion
Ref Expression
eqbrtrd  |-  ( ph  ->  A R C )

Proof of Theorem eqbrtrd
StepHypRef Expression
1 eqbrtrd.2 . 2  |-  ( ph  ->  B R C )
2 eqbrtrd.1 . . 3  |-  ( ph  ->  A  =  B )
32breq1d 4035 . 2  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
41, 3mpbird 223 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625   class class class wbr 4025
This theorem is referenced by:  eqbrtrrd  4047  somin2  5083  en1b  6931  domunsncan  6964  fodomfi  7137  hartogslem1  7259  wemaplem2  7264  infdifsn  7359  carddomi2  7605  cdaun  7800  cda1dif  7804  mapcdaen  7812  cdaxpdom  7817  cdafi  7818  cdainf  7820  carden  8175  alephsuc3  8204  fpwwe2lem6  8259  fpwwe2lem7  8260  inar1  8399  rankcf  8401  lbinfmle  9711  supmul  9724  rpnnen1lem3  10346  xrmin1  10508  xrmin2  10509  ifle  10526  qbtwnxr  10529  xltnegi  10545  xleadd1a  10575  xlt2add  10582  xlemul1a  10610  xov1plusxeqvd  10782  ceim1l  10959  quoremz  10961  quoremnn0ALT  10963  modlt  10983  seqf1olem1  11087  bernneq  11229  discr  11240  faclbnd2  11306  faclbnd4lem3  11310  hashun2  11367  hashfun  11391  sqrlem6  11735  sqrlem7  11736  rddif  11826  amgm2  11855  climconst  12019  rlimconst  12020  serclim0  12053  rlimcn1  12064  mulcn2  12071  reccn2  12072  o1mul  12090  o1rlimmul  12094  iserex  12132  climlec2  12134  iserge0  12136  climcau  12146  caucvgrlem  12147  caucvgr  12150  iseraltlem2  12157  iseraltlem3  12158  iseralt  12159  fsumabs  12261  o1fsum  12273  iserabs  12275  climfsum  12280  isumless  12306  climcndslem2  12311  divrcnv  12313  flo1  12315  supcvg  12316  georeclim  12330  geomulcvg  12334  cvgrat  12341  mertenslem1  12342  efcvgfsum  12369  eftlub  12391  eflegeo  12403  tanhlt1  12442  tanhbnd  12443  ef01bndlem  12466  sin01bnd  12467  cos01bnd  12468  cos01gt0  12473  ruclem2  12512  ruclem3  12513  ruclem9  12518  ruclem11  12520  ruclem12  12521  bitsfzolem  12627  bitsfzo  12628  bitsinv1lem  12634  sadcaddlem  12650  mulgcd  12727  eucalglt  12757  prmind2  12771  mulgcddvds  12785  isprm5  12793  divdenle  12822  nonsq  12832  pythagtriplem4  12874  pclem  12893  pcpremul  12898  pczdvds  12917  pcprmpw2  12936  qexpz  12951  prmreclem4  12968  prmreclem5  12969  4sqlem10  12996  ramtub  13061  ramub2  13063  natpropd  13852  catciso  13941  p0le  14151  acsdomd  14286  divsgrp  14674  oddvds2  14881  odcau  14917  pgpfi  14918  pgpssslw  14927  sylow3lem4  14943  efgred2  15064  frgp0  15071  odadd2  15143  oddvdssubg  15149  ablfac1c  15308  ablfac1eu  15310  pgpfaclem3  15320  isabvd  15587  abvsubtri  15602  cyggic  16528  en2top  16725  1stcrest  17181  2ndcrest  17182  hausmapdom  17228  ufilen  17627  xmetrtri2  17922  prdsxmetlem  17934  bl2in  17959  xblcntr  17965  ssbl  17973  blss  17974  blcld  18053  methaus  18068  nrginvrcnlem  18203  nrginvrcn  18204  nmoi  18239  nmo0  18246  nmoid  18253  blcvx  18306  reperflem  18325  reconnlem2  18334  metdcnlem  18343  metdscn  18362  metnrmlem3  18367  mulc1cncf  18411  iccpnfhmeo  18445  cnheiborlem  18454  cnheibor  18455  lebnumii  18466  pcopt  18522  pcopt2  18523  pcoass  18524  nmoleub2lem  18597  nmoleub2lem3  18598  nmoleub2lem2  18599  ipcau2  18666  tchcphlem1  18667  minveclem3  18795  ivthlem2  18814  ivthlem3  18815  ivth2  18817  ovollb  18840  ovolsslem  18845  ovollb2lem  18849  ovolctb  18851  ovoliunlem1  18863  ovolsca  18876  ovolicc1  18877  ovolicc2lem4  18881  nulmbl  18895  ioombl1lem4  18920  uniioovol  18936  uniioombllem3a  18941  uniioombllem4  18943  opnmbllem  18958  volcn  18963  volivth  18964  i1fadd  19052  i1fmul  19053  mbfi1fseqlem4  19075  mbfi1fseqlem5  19076  mbfi1fseqlem6  19077  itg2const2  19098  itg2seq  19099  itg2uba  19100  itg2split  19106  itg2monolem1  19107  itg2monolem3  19109  itg2i1fseq2  19113  itg2addlem  19115  itg2gt0  19117  itg2cnlem1  19118  itg2cnlem2  19119  itgless  19173  ibladdlem  19176  bddmulibl  19195  dveflem  19328  dvferm1lem  19333  dvferm2lem  19335  dvlip  19342  dvlipcn  19343  dvlip2  19344  dvle  19356  dvivthlem1  19357  lhop1lem  19362  dvcvx  19369  dvfsumabs  19372  dvfsumlem2  19376  dvfsumlem4  19378  dvfsumrlim2  19381  dvfsum2  19383  ftc1a  19386  ftc1lem4  19388  ftc1lem5  19389  deg1sub  19496  ply1divex  19524  deg1submon1p  19540  r1pdeglt  19546  dvdsq1p  19548  fta1glem2  19554  fta1g  19555  plyeq0lem  19594  dgrlt  19649  fta1lem  19689  aalioulem2  19715  aalioulem3  19716  aalioulem4  19717  aaliou3lem2  19725  aaliou3lem9  19732  taylply2  19749  ulmbdd  19777  ulmdvlem1  19779  mtest  19783  radcnvlem1  19791  radcnvle  19798  pserulm  19800  psercn  19804  pserdvlem2  19806  abelthlem2  19810  abelthlem5  19813  abelthlem7  19816  abelthlem8  19817  abelthlem9  19818  reeff1olem  19824  tangtx  19875  tanord  19902  efif1olem4  19909  logrnaddcl  19933  logcj  19962  logimul  19970  logneg2  19971  logdivlti  19973  divlogrlim  19984  logcnlem3  19993  logcnlem4  19994  efopn  20007  logtayllem  20008  logtayl  20009  cxpcn3lem  20089  cxpaddle  20094  abscxpbnd  20095  asinlem3  20169  asinneg  20184  asinsin  20190  atanlogaddlem  20211  atantan  20221  bndatandm  20227  atans2  20229  atantayl  20235  atantayl2  20236  atantayl3  20237  leibpi  20240  birthdaylem3  20250  rlimcnp  20262  efrlim  20266  cxplim  20268  cxp2lim  20273  cxploglim2  20275  divsqrsumo1  20280  jensenlem2  20284  amgm  20287  logdifbnd  20290  harmonicbnd4  20306  fsumharmonic  20307  ftalem1  20312  ftalem5  20316  basellem1  20320  basellem8  20327  ppip1le  20401  ppiltx  20417  sqff1o  20422  chtublem  20452  chpub  20461  logfaclbnd  20463  logfacrlim  20465  logexprlim  20466  mersenne  20468  bcmono  20518  bcmax  20519  bposlem2  20526  bposlem5  20529  lgslem3  20539  lgsquadlem1  20595  lgsquadlem2  20596  2sqblem  20618  chebbnd1  20623  chtppilimlem1  20624  chto1ub  20627  chpchtlim  20630  chpo1ubb  20632  rplogsumlem1  20635  rplogsumlem2  20636  rpvmasumlem  20638  dchrisumlem1  20640  dchrisumlem2  20641  dchrmusum2  20645  dchrvmasumlem2  20649  dchrvmasumlem3  20650  dchrvmasumiflem1  20652  dchrisum0flblem1  20659  dchrisum0fno1  20662  dchrisum0lem1b  20666  dchrisum0lem1  20667  dchrisum0lem2a  20668  dchrisum0lem2  20669  rplogsum  20678  mudivsum  20681  mulogsumlem  20682  mulog2sumlem1  20685  mulog2sumlem2  20686  vmalogdivsum2  20689  2vmadivsumlem  20691  selberglem2  20697  selberg2b  20703  logdivbnd  20707  selberg3lem1  20708  selberg3lem2  20709  selberg4lem1  20711  pntrmax  20715  pntrsumo1  20716  pntrlog2bndlem1  20728  pntrlog2bndlem2  20729  pntrlog2bndlem3  20730  pntrlog2bndlem4  20731  pntrlog2bndlem5  20732  pntrlog2bnd  20735  pntpbnd1a  20736  pntpbnd2  20738  pntibndlem2  20742  pntlemb  20748  pntlemg  20749  pntlemh  20750  pntlemr  20753  pntlemj  20754  pntlemf  20756  pntlemo  20758  pnt  20765  padicabv  20781  ostth2lem2  20785  ostth2lem3  20786  ostth3  20789  nvmtri2  21240  nvabs  21241  nvge0  21242  nvlmle  21267  smcnlem  21272  nmblolbii  21379  blocnilem  21384  siii  21433  ubthlem2  21452  minvecolem3  21457  htthlem  21499  bcsiALT  21760  bcs3  21764  chscllem4  22221  0cnop  22561  0cnfn  22562  nmbdoplbi  22606  nmcoplbi  22610  nmophmi  22613  nmbdfnlbi  22631  nmcfnlbi  22634  nlelchi  22643  riesz1  22647  cnlnadjlem2  22650  nmopadjlei  22670  nmoptrii  22676  nmopcoi  22677  nmopcoadji  22683  unierri  22686  branmfn  22687  pjs14i  22792  hstle  22812  cdj3lem2b  23019  ltesubnnd  23035  ballotlemsel1i  23073  ballotlemro  23083  xlt2addrd  23255  eliccelico  23272  elicoelioo  23273  sqsscirc1  23294  tpr2rico  23298  esumcst  23438  esumpcvgval  23448  measiun  23547  dya2iocct  23583  erdsze2lem1  23736  sinccvglem  24007  nodense  24345  nobnddown  24357  brbtwn2  24535  colinearalglem4  24539  supadd  24928  ltflcei  24930  lxflflp1  24932  itg2addnclem  24933  itg2addnclem2  24934  itg2addnc  24935  mslb1  25618  msra3  25620  fnemeet1  26326  trirn  26474  geomcau  26486  prdsbnd  26528  cntotbnd  26531  heiborlem4  26549  rrndstprj2  26566  rrncmslem  26567  rrnequiv  26570  iccbnd  26575  lzenom  26860  icodiamlt  26916  irrapxlem2  26919  irrapxlem3  26920  irrapxlem5  26922  pellexlem2  26926  pell14qrgt0  26955  pellfundlb  26980  pellfundex  26982  pellfund14  26994  rmspecsqrnq  27002  jm2.24nn  27057  jm2.17a  27058  jm2.17b  27059  congabseq  27072  acongrep  27078  acongeq  27081  jm2.26lem3  27105  jm2.27a  27109  jm2.27c  27111  hbtlem2  27339  dgraaub  27364  f1otrspeq  27401  pmtrfrn  27411  pmtrfconj  27418  symggen  27422  psgnunilem4  27431  idomodle  27523  fmul01  27721  fmul01lt1lem1  27725  fmul01lt1lem2  27726  climrec  27740  climsuse  27745  stoweidlem1  27761  stoweidlem3  27763  stoweidlem11  27771  stoweidlem13  27773  stoweidlem14  27774  stoweidlem16  27776  stoweidlem21  27781  stoweidlem25  27785  stoweidlem26  27786  stoweidlem36  27796  stoweidlem38  27798  stoweidlem41  27801  stoweidlem42  27802  stoweidlem45  27805  stoweidlem48  27808  stoweidlem51  27811  stoweidlem52  27812  stoweidlem62  27822  wallispilem3  27827  stirlinglem1  27834  stirlinglem5  27838  stirlinglem6  27839  stirlinglem7  27840  stirlinglem10  27843  stirlinglem12  27845  stirlinglem15  27848  cvlcvr1  29602  cvrat3  29704  dalem25  29960  cdlema1N  30053  dalawlem3  30135  dalawlem4  30136  dalawlem5  30137  dalawlem6  30138  dalawlem7  30139  dalawlem9  30141  dalawlem11  30143  dalawlem12  30144  lhp2lt  30263  lhpmcvr  30285  4atexlemcnd  30334  lautj  30355  trlle  30446  trlval3  30449  trlval4  30450  cdleme0moN  30487  cdleme13  30534  cdleme15  30540  cdleme19b  30566  cdleme20e  30575  cdleme20j  30580  cdleme22e  30606  cdleme22eALTN  30607  cdleme26fALTN  30624  cdleme26f  30625  cdleme27N  30631  cdleme41sn3a  30695  cdleme46fsvlpq  30767  cdlemeg46vrg  30789  cdlemg4  30879  cdlemg7N  30888  cdlemg9a  30894  cdlemg11b  30904  cdlemg12a  30905  trljco  31002  tendoidcl  31031  tendococl  31034  tendopltp  31042  tendo0tp  31051  tendoicl  31058  cdlemi2  31081  cdlemk5a  31097  cdlemk5  31098  cdlemk12  31112  cdlemkole  31115  cdlemk14  31116  cdlemk12u  31134  cdlemk37  31176  cdlemk39s-id  31202  cdlemk49  31213  cdlemk39u1  31229  cdlemk39u  31230  dian0  31302  cdlemm10N  31381  cdlemn2  31458  cdlemn10  31469  dihord1  31481  dihord10  31486  dihmeetlem4preN  31569  dihmeetlem18N  31587  dihmeetlem20N  31589  dihjatc  31680  mapdcnvatN  31929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026
  Copyright terms: Public domain W3C validator