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

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

Proof of Theorem eqbrtrrd
StepHypRef Expression
1 eqbrtrrd.1 . . 3  |-  ( ph  ->  A  =  B )
21eqcomd 2442 . 2  |-  ( ph  ->  B  =  A )
3 eqbrtrrd.2 . 2  |-  ( ph  ->  A R C )
42, 3eqbrtrd 4233 1  |-  ( ph  ->  B R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   class class class wbr 4213
This theorem is referenced by:  dftpos4  6499  fodomfi  7386  cnfcom2lem  7659  infcda1  8074  enfin1ai  8265  fin56  8274  pwcfsdom  8459  fpwwe2lem7  8512  fpwwe2  8519  canthp1lem1  8528  1nqenq  8840  prlem936  8925  lemulge11  9873  supmul1  9974  xaddge0  10838  xadddi2  10877  ltexp2a  11432  leexp2a  11436  nnlesq  11485  digit1  11514  faclbnd4lem1  11585  faclbnd6  11591  facavg  11593  abs3dif  12136  abs2dif  12137  limsupgre  12276  rlimclim1  12340  rlimuni  12345  rlimres2  12356  rlimcn1  12383  rlimcn1b  12384  recn2  12395  imcn2  12396  rlimo1  12411  o1rlimmul  12413  iserex  12451  isercoll  12462  caucvgrlem2  12469  caucvgr  12470  iseraltlem3  12478  summolem2a  12510  fsumge1  12577  o1fsum  12593  isumrpcl  12624  climcnds  12632  harmonic  12639  mertenslem1  12662  ege2le3  12693  efgt1p2  12716  efgt1p  12717  eirrlem  12804  rpnnen2lem11  12825  fsumdvds  12894  bitsfzo  12948  bitsmod  12949  bitscmp  12951  mulgcd  13047  dvdssqlem  13060  nn0seqcvgd  13062  mulgcddvds  13105  rpdvds  13125  qden1elz  13150  phimullem  13169  pcdvdstr  13250  pockthg  13275  prmreclem1  13285  4sqlem11  13324  ramub1lem1  13395  ramub1lem2  13396  mreexexlem4d  13873  sscid  14025  latmlej21  14522  latmlej22  14523  lubel  14550  efginvrel1  15361  odadd2  15465  odadd  15466  gexexlem  15468  cyggex2  15507  ablfacrplem  15624  ablfac1c  15630  ablfac1eu  15632  pgpfac1lem3a  15635  isabvd  15909  znrrg  16847  lmcn2  17682  metrtri  18388  imasdsf1olem  18404  stdbdxmet  18546  nrmmetd  18623  nmmtri  18669  nlmvscnlem2  18722  blcvx  18830  recld2  18846  zdis  18848  opnreen  18863  cnheibor  18981  lebnumlem3  18989  nmoleub2lem3  19124  nmoleub2lem2  19125  nmoleub3  19128  ipcnlem2  19199  cmetcaulem  19242  cncmet  19276  minveclem4  19334  ovoliunlem1  19399  ovoliun2  19403  ovolscalem1  19410  ovolicopnf  19421  voliunlem2  19446  volsup  19451  ioorcl2  19465  uniiccvol  19473  uniioombllem4  19479  i1fd  19574  mbfi1fseqlem4  19611  itg2const2  19634  itg2eqa  19638  itg2split  19642  itg2i1fseqle  19647  itg2cnlem2  19655  dvcnv  19862  dveflem  19864  dvferm1lem  19869  dvlip2  19880  c1liplem1  19881  dvivthlem1  19893  lhop1lem  19898  dvcvx  19905  dvfsumle  19906  dvfsumabs  19908  dvfsumlem4  19914  dvfsumrlim2  19917  ftc1a  19922  deg1pwle  20043  fta1blem  20092  aalioulem3  20252  aaliou2b  20259  ulmbdd  20315  ulmdvlem1  20317  itgulm  20325  pserdvlem2  20345  abelthlem3  20350  abelthlem5  20352  abelthlem6  20353  abelthlem7  20355  tanregt0  20442  argimlt0  20509  logdivlti  20516  logcnlem3  20536  logcnlem4  20537  logtayl  20552  logtayl2  20554  cxple2  20589  cxpcn3lem  20632  cxpaddle  20637  isosctrlem1  20663  atantayl  20778  efrlim  20809  dfef2  20810  o1cxp  20814  cxp2lim  20816  divsqrsumo1  20823  amgmlem  20829  logdifbnd  20833  emcllem7  20841  harmonicbnd4  20850  fsumharmonic  20851  ftalem2  20857  basellem2  20865  basellem5  20868  basellem9  20872  vma1  20950  sqff1o  20966  fsumfldivdiaglem  20975  chtub  20997  fsumvma2  20999  chpchtsum  21004  chpub  21005  logfaclbnd  21007  logfacbnd3  21008  logfacrlim  21009  logexprlim  21010  bcmono  21062  bposlem2  21070  bposlem5  21073  bposlem6  21074  lgsne0  21118  lgsquadlem1  21139  lgsquadlem2  21140  2sqblem  21162  chebbnd1lem1  21164  chtppilimlem1  21168  chtppilimlem2  21169  chpchtlim  21174  rplogsumlem1  21179  dchrvmasumiflem1  21196  dchrisum0flblem2  21204  dchrisum0fno1  21206  dchrisum0re  21208  dchrisum0lem2a  21212  dchrisum0lem3  21214  dirith  21224  mulog2sumlem1  21229  mulog2sumlem2  21230  log2sumbnd  21239  selberglem2  21241  logdivbnd  21251  selberg3lem1  21252  selberg4lem1  21255  pntrsumbnd2  21262  pntrlog2bndlem1  21272  pntrlog2bndlem5  21276  pntrlog2bndlem6  21278  pntpbnd1a  21280  pntpbnd1  21281  pntpbnd2  21282  pntibndlem3  21287  pntlemb  21292  pntlemn  21295  pntlemr  21297  pntlemj  21298  pntlemf  21300  pntlemo  21302  ostth2lem3  21330  ostth3  21333  nvabs  22163  nvlmle  22189  smcnlem  22194  ubthlem2  22374  minvecolem4  22383  htthlem  22421  normpyc  22649  nmophmi  23535  hstle  23734  hstles  23735  stlei  23744  xrge0npcan  24217  esumpinfval  24464  esumpinfsum  24468  esumpcvgval  24469  dya2icoseg  24628  lgamgulmlem2  24815  lgamgulmlem3  24816  lgamucov  24823  lgamcvg2  24840  gamcvg2  24845  rescon  24934  sinccvglem  25110  circum  25112  prodmolem2a  25261  btwnxfr  25991  supaddc  26238  mblfinlem3  26246  mblfinlem4  26247  itg2addnclem3  26259  ftc1anc  26289  nn0prpwlem  26326  csbrn  26457  trirn  26458  isbnd3  26494  cntotbnd  26506  bfp  26534  rrndstprj2  26541  irrapxlem1  26886  irrapxlem4  26889  pell1qrgaplem  26937  pellfundglb  26949  rmspecfund  26973  monotoddzzfi  27006  rmynn  27022  jm2.24nn  27025  jm2.17c  27028  jm2.24  27029  acongeq  27049  jm2.20nn  27069  jm2.26lem3  27073  jm2.27a  27077  jm2.27c  27079  rmydioph  27086  jm3.1lem2  27090  frlmpwfi  27240  f1linds  27273  hashgcdlem  27494  hashgcdeq  27495  cncmpmax  27680  fmul01lt1lem2  27692  clim1fr1  27704  stoweidlem1  27727  stoweidlem11  27737  stoweidlem14  27740  stoweidlem24  27750  stoweidlem26  27752  wallispilem4  27794  wallispilem5  27795  stirlinglem1  27800  2leaddle2  28093  isosctrlem1ALT  29047  1cvrjat  30273  3atlem1  30281  3atlem6  30286  llnmlplnN  30337  2llnjaN  30364  2lplnja  30417  dalem57  30527  dalawlem11  30679  dalawlem12  30680  lhp2lt  30799  lhpj1  30820  lhpm0atN  30827  4atexlemex2  30869  lautm  30892  cdleme17b  31085  cdleme20j  31116  cdleme30a  31176  cdlemg4c  31410  cdlemg17a  31459  cdlemg31c  31497  trljco  31538  cdlemk46  31746  dia2dimlem2  31864  cdlemm10N  31917  cdlemn10  32005  dihmeetlem1N  32089  dihglblem5apreN  32090  dihmeetlem15N  32120  mapdat  32466
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-rab 2715  df-v 2959  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-sn 3821  df-pr 3822  df-op 3824  df-br 4214
  Copyright terms: Public domain W3C validator