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

Theorem eqbrtrd 4043
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 4033 . 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 1623   class class class wbr 4023
This theorem is referenced by:  eqbrtrrd  4045  somin2  5081  en1b  6929  domunsncan  6962  fodomfi  7135  hartogslem1  7257  wemaplem2  7262  infdifsn  7357  carddomi2  7603  cdaun  7798  cda1dif  7802  mapcdaen  7810  cdaxpdom  7815  cdafi  7816  cdainf  7818  carden  8173  alephsuc3  8202  fpwwe2lem6  8257  fpwwe2lem7  8258  inar1  8397  rankcf  8399  lbinfmle  9709  supmul  9722  rpnnen1lem3  10344  xrmin1  10506  xrmin2  10507  ifle  10524  qbtwnxr  10527  xltnegi  10543  xleadd1a  10573  xlt2add  10580  xlemul1a  10608  xov1plusxeqvd  10780  ceim1l  10957  quoremz  10959  quoremnn0ALT  10961  modlt  10981  seqf1olem1  11085  bernneq  11227  discr  11238  faclbnd2  11304  faclbnd4lem3  11308  hashun2  11365  hashfun  11389  sqrlem6  11733  sqrlem7  11734  rddif  11824  amgm2  11853  climconst  12017  rlimconst  12018  serclim0  12051  rlimcn1  12062  mulcn2  12069  reccn2  12070  o1mul  12088  o1rlimmul  12092  iserex  12130  climlec2  12132  iserge0  12134  climcau  12144  caucvgrlem  12145  caucvgr  12148  iseraltlem2  12155  iseraltlem3  12156  iseralt  12157  fsumabs  12259  o1fsum  12271  iserabs  12273  climfsum  12278  isumless  12304  climcndslem2  12309  divrcnv  12311  flo1  12313  supcvg  12314  georeclim  12328  geomulcvg  12332  cvgrat  12339  mertenslem1  12340  efcvgfsum  12367  eftlub  12389  eflegeo  12401  tanhlt1  12440  tanhbnd  12441  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  cos01gt0  12471  ruclem2  12510  ruclem3  12511  ruclem9  12516  ruclem11  12518  ruclem12  12519  bitsfzolem  12625  bitsfzo  12626  bitsinv1lem  12632  sadcaddlem  12648  mulgcd  12725  eucalglt  12755  prmind2  12769  mulgcddvds  12783  isprm5  12791  divdenle  12820  nonsq  12830  pythagtriplem4  12872  pclem  12891  pcpremul  12896  pczdvds  12915  pcprmpw2  12934  qexpz  12949  prmreclem4  12966  prmreclem5  12967  4sqlem10  12994  ramtub  13059  ramub2  13061  natpropd  13850  catciso  13939  p0le  14149  acsdomd  14284  divsgrp  14672  oddvds2  14879  odcau  14915  pgpfi  14916  pgpssslw  14925  sylow3lem4  14941  efgred2  15062  frgp0  15069  odadd2  15141  oddvdssubg  15147  ablfac1c  15306  ablfac1eu  15308  pgpfaclem3  15318  isabvd  15585  abvsubtri  15600  cyggic  16526  en2top  16723  1stcrest  17179  2ndcrest  17180  hausmapdom  17226  ufilen  17625  xmetrtri2  17920  prdsxmetlem  17932  bl2in  17957  xblcntr  17963  ssbl  17971  blss  17972  blcld  18051  methaus  18066  nrginvrcnlem  18201  nrginvrcn  18202  nmoi  18237  nmo0  18244  nmoid  18251  blcvx  18304  reperflem  18323  reconnlem2  18332  metdcnlem  18341  metdscn  18360  metnrmlem3  18365  mulc1cncf  18409  iccpnfhmeo  18443  cnheiborlem  18452  cnheibor  18453  lebnumii  18464  pcopt  18520  pcopt2  18521  pcoass  18522  nmoleub2lem  18595  nmoleub2lem3  18596  nmoleub2lem2  18597  ipcau2  18664  tchcphlem1  18665  minveclem3  18793  ivthlem2  18812  ivthlem3  18813  ivth2  18815  ovollb  18838  ovolsslem  18843  ovollb2lem  18847  ovolctb  18849  ovoliunlem1  18861  ovolsca  18874  ovolicc1  18875  ovolicc2lem4  18879  nulmbl  18893  ioombl1lem4  18918  uniioovol  18934  uniioombllem3a  18939  uniioombllem4  18941  opnmbllem  18956  volcn  18961  volivth  18962  i1fadd  19050  i1fmul  19051  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1fseqlem6  19075  itg2const2  19096  itg2seq  19097  itg2uba  19098  itg2split  19104  itg2monolem1  19105  itg2monolem3  19107  itg2i1fseq2  19111  itg2addlem  19113  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  itgless  19171  ibladdlem  19174  bddmulibl  19193  dveflem  19326  dvferm1lem  19331  dvferm2lem  19333  dvlip  19340  dvlipcn  19341  dvlip2  19342  dvle  19354  dvivthlem1  19355  lhop1lem  19360  dvcvx  19367  dvfsumabs  19370  dvfsumlem2  19374  dvfsumlem4  19376  dvfsumrlim2  19379  dvfsum2  19381  ftc1a  19384  ftc1lem4  19386  ftc1lem5  19387  deg1sub  19494  ply1divex  19522  deg1submon1p  19538  r1pdeglt  19544  dvdsq1p  19546  fta1glem2  19552  fta1g  19553  plyeq0lem  19592  dgrlt  19647  fta1lem  19687  aalioulem2  19713  aalioulem3  19714  aalioulem4  19715  aaliou3lem2  19723  aaliou3lem9  19730  taylply2  19747  ulmbdd  19775  ulmdvlem1  19777  mtest  19781  radcnvlem1  19789  radcnvle  19796  pserulm  19798  psercn  19802  pserdvlem2  19804  abelthlem2  19808  abelthlem5  19811  abelthlem7  19814  abelthlem8  19815  abelthlem9  19816  reeff1olem  19822  tangtx  19873  tanord  19900  efif1olem4  19907  logrnaddcl  19931  logcj  19960  logimul  19968  logneg2  19969  logdivlti  19971  divlogrlim  19982  logcnlem3  19991  logcnlem4  19992  efopn  20005  logtayllem  20006  logtayl  20007  cxpcn3lem  20087  cxpaddle  20092  abscxpbnd  20093  asinlem3  20167  asinneg  20182  asinsin  20188  atanlogaddlem  20209  atantan  20219  bndatandm  20225  atans2  20227  atantayl  20233  atantayl2  20234  atantayl3  20235  leibpi  20238  birthdaylem3  20248  rlimcnp  20260  efrlim  20264  cxplim  20266  cxp2lim  20271  cxploglim2  20273  divsqrsumo1  20278  jensenlem2  20282  amgm  20285  logdifbnd  20288  harmonicbnd4  20304  fsumharmonic  20305  ftalem1  20310  ftalem5  20314  basellem1  20318  basellem8  20325  ppip1le  20399  ppiltx  20415  sqff1o  20420  chtublem  20450  chpub  20459  logfaclbnd  20461  logfacrlim  20463  logexprlim  20464  mersenne  20466  bcmono  20516  bcmax  20517  bposlem2  20524  bposlem5  20527  lgslem3  20537  lgsquadlem1  20593  lgsquadlem2  20594  2sqblem  20616  chebbnd1  20621  chtppilimlem1  20622  chto1ub  20625  chpchtlim  20628  chpo1ubb  20630  rplogsumlem1  20633  rplogsumlem2  20634  rpvmasumlem  20636  dchrisumlem1  20638  dchrisumlem2  20639  dchrmusum2  20643  dchrvmasumlem2  20647  dchrvmasumlem3  20648  dchrvmasumiflem1  20650  dchrisum0flblem1  20657  dchrisum0fno1  20660  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  rplogsum  20676  mudivsum  20679  mulogsumlem  20680  mulog2sumlem1  20683  mulog2sumlem2  20684  vmalogdivsum2  20687  2vmadivsumlem  20689  selberglem2  20695  selberg2b  20701  logdivbnd  20705  selberg3lem1  20706  selberg3lem2  20707  selberg4lem1  20709  pntrmax  20713  pntrsumo1  20714  pntrlog2bndlem1  20726  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bnd  20733  pntpbnd1a  20734  pntpbnd2  20736  pntibndlem2  20740  pntlemb  20746  pntlemg  20747  pntlemh  20748  pntlemr  20751  pntlemj  20752  pntlemf  20754  pntlemo  20756  pnt  20763  padicabv  20779  ostth2lem2  20783  ostth2lem3  20784  ostth3  20787  nvmtri2  21238  nvabs  21239  nvge0  21240  nvlmle  21265  smcnlem  21270  nmblolbii  21377  blocnilem  21382  siii  21431  ubthlem2  21450  minvecolem3  21455  htthlem  21497  bcsiALT  21758  bcs3  21762  chscllem4  22219  0cnop  22559  0cnfn  22560  nmbdoplbi  22604  nmcoplbi  22608  nmophmi  22611  nmbdfnlbi  22629  nmcfnlbi  22632  nlelchi  22641  riesz1  22645  cnlnadjlem2  22648  nmopadjlei  22668  nmoptrii  22674  nmopcoi  22675  nmopcoadji  22681  unierri  22684  branmfn  22685  pjs14i  22790  hstle  22810  cdj3lem2b  23017  ltesubnnd  23033  ballotlemsel1i  23071  ballotlemro  23081  xlt2addrd  23253  eliccelico  23270  elicoelioo  23271  sqsscirc1  23292  tpr2rico  23296  esumcst  23436  esumpcvgval  23446  measiun  23545  dya2iocct  23581  erdsze2lem1  23734  sinccvglem  24005  nodense  24343  nobnddown  24355  brbtwn2  24533  colinearalglem4  24537  mslb1  25607  msra3  25609  fnemeet1  26315  trirn  26463  geomcau  26475  prdsbnd  26517  cntotbnd  26520  heiborlem4  26538  rrndstprj2  26555  rrncmslem  26556  rrnequiv  26559  iccbnd  26564  lzenom  26849  icodiamlt  26905  irrapxlem2  26908  irrapxlem3  26909  irrapxlem5  26911  pellexlem2  26915  pell14qrgt0  26944  pellfundlb  26969  pellfundex  26971  pellfund14  26983  rmspecsqrnq  26991  jm2.24nn  27046  jm2.17a  27047  jm2.17b  27048  congabseq  27061  acongrep  27067  acongeq  27070  jm2.26lem3  27094  jm2.27a  27098  jm2.27c  27100  hbtlem2  27328  dgraaub  27353  f1otrspeq  27390  pmtrfrn  27400  pmtrfconj  27407  symggen  27411  psgnunilem4  27420  idomodle  27512  fmul01  27710  fmul01lt1lem1  27714  fmul01lt1lem2  27715  climrec  27729  climsuse  27734  stoweidlem1  27750  stoweidlem3  27752  stoweidlem11  27760  stoweidlem13  27762  stoweidlem14  27763  stoweidlem16  27765  stoweidlem21  27770  stoweidlem25  27774  stoweidlem26  27775  stoweidlem36  27785  stoweidlem38  27787  stoweidlem41  27790  stoweidlem42  27791  stoweidlem45  27794  stoweidlem48  27797  stoweidlem51  27800  stoweidlem52  27801  stoweidlem62  27811  wallispilem3  27816  stirlinglem1  27823  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem10  27832  stirlinglem12  27834  stirlinglem15  27837  cvlcvr1  29529  cvrat3  29631  dalem25  29887  cdlema1N  29980  dalawlem3  30062  dalawlem4  30063  dalawlem5  30064  dalawlem6  30065  dalawlem7  30066  dalawlem9  30068  dalawlem11  30070  dalawlem12  30071  lhp2lt  30190  lhpmcvr  30212  4atexlemcnd  30261  lautj  30282  trlle  30373  trlval3  30376  trlval4  30377  cdleme0moN  30414  cdleme13  30461  cdleme15  30467  cdleme19b  30493  cdleme20e  30502  cdleme20j  30507  cdleme22e  30533  cdleme22eALTN  30534  cdleme26fALTN  30551  cdleme26f  30552  cdleme27N  30558  cdleme41sn3a  30622  cdleme46fsvlpq  30694  cdlemeg46vrg  30716  cdlemg4  30806  cdlemg7N  30815  cdlemg9a  30821  cdlemg11b  30831  cdlemg12a  30832  trljco  30929  tendoidcl  30958  tendococl  30961  tendopltp  30969  tendo0tp  30978  tendoicl  30985  cdlemi2  31008  cdlemk5a  31024  cdlemk5  31025  cdlemk12  31039  cdlemkole  31042  cdlemk14  31043  cdlemk12u  31061  cdlemk37  31103  cdlemk39s-id  31129  cdlemk49  31140  cdlemk39u1  31156  cdlemk39u  31157  dian0  31229  cdlemm10N  31308  cdlemn2  31385  cdlemn10  31396  dihord1  31408  dihord10  31413  dihmeetlem4preN  31496  dihmeetlem18N  31514  dihmeetlem20N  31516  dihjatc  31607  mapdcnvatN  31856
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator