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

Theorem eqbrtrd 4044
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 4034 . 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 4024
This theorem is referenced by:  eqbrtrrd  4046  somin2  5080  en1b  6925  domunsncan  6958  fodomfi  7131  hartogslem1  7253  wemaplem2  7258  infdifsn  7353  carddomi2  7599  cdaun  7794  cda1dif  7798  mapcdaen  7806  cdaxpdom  7811  cdafi  7812  cdainf  7814  carden  8169  alephsuc3  8198  fpwwe2lem6  8253  fpwwe2lem7  8254  inar1  8393  rankcf  8395  lbinfmle  9705  supmul  9718  rpnnen1lem3  10340  xrmin1  10502  xrmin2  10503  ifle  10520  qbtwnxr  10523  xltnegi  10539  xleadd1a  10569  xlt2add  10576  xlemul1a  10604  xov1plusxeqvd  10776  ceim1l  10953  quoremz  10955  quoremnn0  10957  modlt  10977  seqf1olem1  11081  bernneq  11223  discr  11234  faclbnd2  11300  faclbnd4lem3  11304  hashun2  11361  hashfun  11385  sqrlem6  11729  sqrlem7  11730  rddif  11820  amgm2  11849  climconst  12013  rlimconst  12014  serclim0  12047  rlimcn1  12058  mulcn2  12065  reccn2  12066  o1mul  12084  o1rlimmul  12088  iserex  12126  climlec2  12128  iserge0  12130  climcau  12140  caucvgrlem  12141  caucvgr  12144  iseraltlem2  12151  iseraltlem3  12152  iseralt  12153  fsumabs  12255  o1fsum  12267  iserabs  12269  climfsum  12274  isumless  12300  climcndslem2  12305  divrcnv  12307  flo1  12309  supcvg  12310  georeclim  12324  geomulcvg  12328  cvgrat  12335  mertenslem1  12336  efcvgfsum  12363  eftlub  12385  eflegeo  12397  tanhlt1  12436  tanhbnd  12437  ef01bndlem  12460  sin01bnd  12461  cos01bnd  12462  cos01gt0  12467  ruclem2  12506  ruclem3  12507  ruclem9  12512  ruclem11  12514  ruclem12  12515  bitsfzolem  12621  bitsfzo  12622  bitsinv1lem  12628  sadcaddlem  12644  mulgcd  12721  eucalglt  12751  prmind2  12765  mulgcddvds  12779  isprm5  12787  divdenle  12816  nonsq  12826  pythagtriplem4  12868  pclem  12887  pcpremul  12892  pczdvds  12911  pcprmpw2  12930  qexpz  12945  prmreclem4  12962  prmreclem5  12963  4sqlem10  12990  ramtub  13055  ramub2  13057  natpropd  13846  catciso  13935  p0le  14145  acsdomd  14280  divsgrp  14668  oddvds2  14875  odcau  14911  pgpfi  14912  pgpssslw  14921  sylow3lem4  14937  efgred2  15058  frgp0  15065  odadd2  15137  oddvdssubg  15143  ablfac1c  15302  ablfac1eu  15304  pgpfaclem3  15314  isabvd  15581  abvsubtri  15596  cyggic  16522  en2top  16719  1stcrest  17175  2ndcrest  17176  hausmapdom  17222  ufilen  17621  xmetrtri2  17916  prdsxmetlem  17928  bl2in  17953  xblcntr  17959  ssbl  17967  blss  17968  blcld  18047  methaus  18062  nrginvrcnlem  18197  nrginvrcn  18198  nmoi  18233  nmo0  18240  nmoid  18247  blcvx  18300  reperflem  18319  reconnlem2  18328  metdcnlem  18337  metdscn  18356  metnrmlem3  18361  mulc1cncf  18405  iccpnfhmeo  18439  cnheiborlem  18448  cnheibor  18449  lebnumii  18460  pcopt  18516  pcopt2  18517  pcoass  18518  nmoleub2lem  18591  nmoleub2lem3  18592  nmoleub2lem2  18593  ipcau2  18660  tchcphlem1  18661  minveclem3  18789  ivthlem2  18808  ivthlem3  18809  ivth2  18811  ovollb  18834  ovolsslem  18839  ovollb2lem  18843  ovolctb  18845  ovoliunlem1  18857  ovolsca  18870  ovolicc1  18871  ovolicc2lem4  18875  nulmbl  18889  ioombl1lem4  18914  uniioovol  18930  uniioombllem3a  18935  uniioombllem4  18937  opnmbllem  18952  volcn  18957  volivth  18958  i1fadd  19046  i1fmul  19047  mbfi1fseqlem4  19069  mbfi1fseqlem5  19070  mbfi1fseqlem6  19071  itg2const2  19092  itg2seq  19093  itg2uba  19094  itg2split  19100  itg2monolem1  19101  itg2monolem3  19103  itg2i1fseq2  19107  itg2addlem  19109  itg2gt0  19111  itg2cnlem1  19112  itg2cnlem2  19113  itgless  19167  ibladdlem  19170  bddmulibl  19189  dveflem  19322  dvferm1lem  19327  dvferm2lem  19329  dvlip  19336  dvlipcn  19337  dvlip2  19338  dvle  19350  dvivthlem1  19351  lhop1lem  19356  dvcvx  19363  dvfsumabs  19366  dvfsumlem2  19370  dvfsumlem4  19372  dvfsumrlim2  19375  dvfsum2  19377  ftc1a  19380  ftc1lem4  19382  ftc1lem5  19383  deg1sub  19490  ply1divex  19518  deg1submon1p  19534  r1pdeglt  19540  dvdsq1p  19542  fta1glem2  19548  fta1g  19549  plyeq0lem  19588  dgrlt  19643  fta1lem  19683  aalioulem2  19709  aalioulem3  19710  aalioulem4  19711  aaliou3lem2  19719  aaliou3lem9  19726  taylply2  19743  ulmbdd  19771  ulmdvlem1  19773  mtest  19777  radcnvlem1  19785  radcnvle  19792  pserulm  19794  psercn  19798  pserdvlem2  19800  abelthlem2  19804  abelthlem5  19807  abelthlem7  19810  abelthlem8  19811  abelthlem9  19812  reeff1olem  19818  tangtx  19869  tanord  19896  efif1olem4  19903  logrnaddcl  19927  logcj  19956  logimul  19964  logneg2  19965  logdivlti  19967  divlogrlim  19978  logcnlem3  19987  logcnlem4  19988  efopn  20001  logtayllem  20002  logtayl  20003  cxpcn3lem  20083  cxpaddle  20088  abscxpbnd  20089  asinlem3  20163  asinneg  20178  asinsin  20184  atanlogaddlem  20205  atantan  20215  bndatandm  20221  atans2  20223  atantayl  20229  atantayl2  20230  atantayl3  20231  leibpi  20234  birthdaylem3  20244  rlimcnp  20256  efrlim  20260  cxplim  20262  cxp2lim  20267  cxploglim2  20269  divsqrsumo1  20274  jensenlem2  20278  amgm  20281  logdifbnd  20284  harmonicbnd4  20300  fsumharmonic  20301  ftalem1  20306  ftalem5  20310  basellem1  20314  basellem8  20321  ppip1le  20395  ppiltx  20411  sqff1o  20416  chtublem  20446  chpub  20455  logfaclbnd  20457  logfacrlim  20459  logexprlim  20460  mersenne  20462  bcmono  20512  bcmax  20513  bposlem2  20520  bposlem5  20523  lgslem3  20533  lgsquadlem1  20589  lgsquadlem2  20590  2sqblem  20612  chebbnd1  20617  chtppilimlem1  20618  chto1ub  20621  chpchtlim  20624  chpo1ubb  20626  rplogsumlem1  20629  rplogsumlem2  20630  rpvmasumlem  20632  dchrisumlem1  20634  dchrisumlem2  20635  dchrmusum2  20639  dchrvmasumlem2  20643  dchrvmasumlem3  20644  dchrvmasumiflem1  20646  dchrisum0flblem1  20653  dchrisum0fno1  20656  dchrisum0lem1b  20660  dchrisum0lem1  20661  dchrisum0lem2a  20662  dchrisum0lem2  20663  rplogsum  20672  mudivsum  20675  mulogsumlem  20676  mulog2sumlem1  20679  mulog2sumlem2  20680  vmalogdivsum2  20683  2vmadivsumlem  20685  selberglem2  20691  selberg2b  20697  logdivbnd  20701  selberg3lem1  20702  selberg3lem2  20703  selberg4lem1  20705  pntrmax  20709  pntrsumo1  20710  pntrlog2bndlem1  20722  pntrlog2bndlem2  20723  pntrlog2bndlem3  20724  pntrlog2bndlem4  20725  pntrlog2bndlem5  20726  pntrlog2bnd  20729  pntpbnd1a  20730  pntpbnd2  20732  pntibndlem2  20736  pntlemb  20742  pntlemg  20743  pntlemh  20744  pntlemr  20747  pntlemj  20748  pntlemf  20750  pntlemo  20752  pnt  20759  padicabv  20775  ostth2lem2  20779  ostth2lem3  20780  ostth3  20783  nvmtri2  21232  nvabs  21233  nvge0  21234  nvlmle  21259  smcnlem  21264  nmblolbii  21371  blocnilem  21376  siii  21425  ubthlem2  21444  minvecolem3  21449  htthlem  21491  bcsiALT  21754  bcs3  21758  chscllem4  22215  0cnop  22555  0cnfn  22556  nmbdoplbi  22600  nmcoplbi  22604  nmophmi  22607  nmbdfnlbi  22625  nmcfnlbi  22628  nlelchi  22637  riesz1  22641  cnlnadjlem2  22644  nmopadjlei  22664  nmoptrii  22670  nmopcoi  22671  nmopcoadji  22677  unierri  22680  branmfn  22681  pjs14i  22786  hstle  22806  cdj3lem2b  23013  ltesubnnd  23029  ballotlemsel1i  23067  ballotlemro  23077  erdsze2lem1  23141  sinccvglem  23412  axdense  23747  axfelem10  23759  brbtwn2  23943  colinearalglem4  23947  mslb1  25018  msra3  25020  fnemeet1  25726  trirn  25874  geomcau  25886  prdsbnd  25928  cntotbnd  25931  heiborlem4  25949  rrndstprj2  25966  rrncmslem  25967  rrnequiv  25970  iccbnd  25975  lzenom  26260  icodiamlt  26316  irrapxlem2  26319  irrapxlem3  26320  irrapxlem5  26322  pellexlem2  26326  pell14qrgt0  26355  pellfundlb  26380  pellfundex  26382  pellfund14  26394  rmspecsqrnq  26402  jm2.24nn  26457  jm2.17a  26458  jm2.17b  26459  congabseq  26472  acongrep  26478  acongeq  26481  jm2.26lem3  26505  jm2.27a  26509  jm2.27c  26511  hbtlem2  26739  dgraaub  26764  f1otrspeq  26801  pmtrfrn  26811  pmtrfconj  26818  symggen  26822  psgnunilem4  26831  idomodle  26923  fmul01  27121  fmul01lt1lem1  27125  fmul01lt1lem2  27126  climrec  27140  climsuse  27145  stoweidlem1  27161  stoweidlem3  27163  stoweidlem11  27171  stoweidlem13  27173  stoweidlem14  27174  stoweidlem16  27176  stoweidlem21  27181  stoweidlem25  27185  stoweidlem26  27186  stoweidlem36  27196  stoweidlem38  27198  stoweidlem41  27201  stoweidlem42  27202  stoweidlem45  27205  stoweidlem48  27208  stoweidlem51  27211  stoweidlem52  27212  stoweidlem62  27222  wallispilem3  27227  stirlinglem1  27234  stirlinglem5  27238  stirlinglem6  27239  stirlinglem7  27240  stirlinglem10  27243  stirlinglem12  27245  stirlinglem15  27248  cvlcvr1  28808  cvrat3  28910  dalem25  29166  cdlema1N  29259  dalawlem3  29341  dalawlem4  29342  dalawlem5  29343  dalawlem6  29344  dalawlem7  29345  dalawlem9  29347  dalawlem11  29349  dalawlem12  29350  lhp2lt  29469  lhpmcvr  29491  4atexlemcnd  29540  lautj  29561  trlle  29652  trlval3  29655  trlval4  29656  cdleme0moN  29693  cdleme13  29740  cdleme15  29746  cdleme19b  29772  cdleme20e  29781  cdleme20j  29786  cdleme22e  29812  cdleme22eALTN  29813  cdleme26fALTN  29830  cdleme26f  29831  cdleme27N  29837  cdleme41sn3a  29901  cdleme46fsvlpq  29973  cdlemeg46vrg  29995  cdlemg4  30085  cdlemg7N  30094  cdlemg9a  30100  cdlemg11b  30110  cdlemg12a  30111  trljco  30208  tendoidcl  30237  tendococl  30240  tendopltp  30248  tendo0tp  30257  tendoicl  30264  cdlemi2  30287  cdlemk5a  30303  cdlemk5  30304  cdlemk12  30318  cdlemkole  30321  cdlemk14  30322  cdlemk12u  30340  cdlemk37  30382  cdlemk39s-id  30408  cdlemk49  30419  cdlemk39u1  30435  cdlemk39u  30436  dian0  30508  cdlemm10N  30587  cdlemn2  30664  cdlemn10  30675  dihord1  30687  dihord10  30692  dihmeetlem4preN  30775  dihmeetlem18N  30793  dihmeetlem20N  30795  dihjatc  30886  mapdcnvatN  31135
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025
  Copyright terms: Public domain W3C validator