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

Theorem eqbrtrd 4059
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 4049 . 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 1632   class class class wbr 4039
This theorem is referenced by:  eqbrtrrd  4061  somin2  5097  en1b  6945  domunsncan  6978  fodomfi  7151  hartogslem1  7273  wemaplem2  7278  infdifsn  7373  carddomi2  7619  cdaun  7814  cda1dif  7818  mapcdaen  7826  cdaxpdom  7831  cdafi  7832  cdainf  7834  carden  8189  alephsuc3  8218  fpwwe2lem6  8273  fpwwe2lem7  8274  inar1  8413  rankcf  8415  lbinfmle  9725  supmul  9738  rpnnen1lem3  10360  xrmin1  10522  xrmin2  10523  ifle  10540  qbtwnxr  10543  xltnegi  10559  xleadd1a  10589  xlt2add  10596  xlemul1a  10624  xov1plusxeqvd  10796  ceim1l  10973  quoremz  10975  quoremnn0ALT  10977  modlt  10997  seqf1olem1  11101  bernneq  11243  discr  11254  faclbnd2  11320  faclbnd4lem3  11324  hashun2  11381  hashfun  11405  sqrlem6  11749  sqrlem7  11750  rddif  11840  amgm2  11869  climconst  12033  rlimconst  12034  serclim0  12067  rlimcn1  12078  mulcn2  12085  reccn2  12086  o1mul  12104  o1rlimmul  12108  iserex  12146  climlec2  12148  iserge0  12150  climcau  12160  caucvgrlem  12161  caucvgr  12164  iseraltlem2  12171  iseraltlem3  12172  iseralt  12173  fsumabs  12275  o1fsum  12287  iserabs  12289  climfsum  12294  isumless  12320  climcndslem2  12325  divrcnv  12327  flo1  12329  supcvg  12330  georeclim  12344  geomulcvg  12348  cvgrat  12355  mertenslem1  12356  efcvgfsum  12383  eftlub  12405  eflegeo  12417  tanhlt1  12456  tanhbnd  12457  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  cos01gt0  12487  ruclem2  12526  ruclem3  12527  ruclem9  12532  ruclem11  12534  ruclem12  12535  bitsfzolem  12641  bitsfzo  12642  bitsinv1lem  12648  sadcaddlem  12664  mulgcd  12741  eucalglt  12771  prmind2  12785  mulgcddvds  12799  isprm5  12807  divdenle  12836  nonsq  12846  pythagtriplem4  12888  pclem  12907  pcpremul  12912  pczdvds  12931  pcprmpw2  12950  qexpz  12965  prmreclem4  12982  prmreclem5  12983  4sqlem10  13010  ramtub  13075  ramub2  13077  natpropd  13866  catciso  13955  p0le  14165  acsdomd  14300  divsgrp  14688  oddvds2  14895  odcau  14931  pgpfi  14932  pgpssslw  14941  sylow3lem4  14957  efgred2  15078  frgp0  15085  odadd2  15157  oddvdssubg  15163  ablfac1c  15322  ablfac1eu  15324  pgpfaclem3  15334  isabvd  15601  abvsubtri  15616  cyggic  16542  en2top  16739  1stcrest  17195  2ndcrest  17196  hausmapdom  17242  ufilen  17641  xmetrtri2  17936  prdsxmetlem  17948  bl2in  17973  xblcntr  17979  ssbl  17987  blss  17988  blcld  18067  methaus  18082  nrginvrcnlem  18217  nrginvrcn  18218  nmoi  18253  nmo0  18260  nmoid  18267  blcvx  18320  reperflem  18339  reconnlem2  18348  metdcnlem  18357  metdscn  18376  metnrmlem3  18381  mulc1cncf  18425  iccpnfhmeo  18459  cnheiborlem  18468  cnheibor  18469  lebnumii  18480  pcopt  18536  pcopt2  18537  pcoass  18538  nmoleub2lem  18611  nmoleub2lem3  18612  nmoleub2lem2  18613  ipcau2  18680  tchcphlem1  18681  minveclem3  18809  ivthlem2  18828  ivthlem3  18829  ivth2  18831  ovollb  18854  ovolsslem  18859  ovollb2lem  18863  ovolctb  18865  ovoliunlem1  18877  ovolsca  18890  ovolicc1  18891  ovolicc2lem4  18895  nulmbl  18909  ioombl1lem4  18934  uniioovol  18950  uniioombllem3a  18955  uniioombllem4  18957  opnmbllem  18972  volcn  18977  volivth  18978  i1fadd  19066  i1fmul  19067  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  mbfi1fseqlem6  19091  itg2const2  19112  itg2seq  19113  itg2uba  19114  itg2split  19120  itg2monolem1  19121  itg2monolem3  19123  itg2i1fseq2  19127  itg2addlem  19129  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  itgless  19187  ibladdlem  19190  bddmulibl  19209  dveflem  19342  dvferm1lem  19347  dvferm2lem  19349  dvlip  19356  dvlipcn  19357  dvlip2  19358  dvle  19370  dvivthlem1  19371  lhop1lem  19376  dvcvx  19383  dvfsumabs  19386  dvfsumlem2  19390  dvfsumlem4  19392  dvfsumrlim2  19395  dvfsum2  19397  ftc1a  19400  ftc1lem4  19402  ftc1lem5  19403  deg1sub  19510  ply1divex  19538  deg1submon1p  19554  r1pdeglt  19560  dvdsq1p  19562  fta1glem2  19568  fta1g  19569  plyeq0lem  19608  dgrlt  19663  fta1lem  19703  aalioulem2  19729  aalioulem3  19730  aalioulem4  19731  aaliou3lem2  19739  aaliou3lem9  19746  taylply2  19763  ulmbdd  19791  ulmdvlem1  19793  mtest  19797  radcnvlem1  19805  radcnvle  19812  pserulm  19814  psercn  19818  pserdvlem2  19820  abelthlem2  19824  abelthlem5  19827  abelthlem7  19830  abelthlem8  19831  abelthlem9  19832  reeff1olem  19838  tangtx  19889  tanord  19916  efif1olem4  19923  logrnaddcl  19947  logcj  19976  logimul  19984  logneg2  19985  logdivlti  19987  divlogrlim  19998  logcnlem3  20007  logcnlem4  20008  efopn  20021  logtayllem  20022  logtayl  20023  cxpcn3lem  20103  cxpaddle  20108  abscxpbnd  20109  asinlem3  20183  asinneg  20198  asinsin  20204  atanlogaddlem  20225  atantan  20235  bndatandm  20241  atans2  20243  atantayl  20249  atantayl2  20250  atantayl3  20251  leibpi  20254  birthdaylem3  20264  rlimcnp  20276  efrlim  20280  cxplim  20282  cxp2lim  20287  cxploglim2  20289  divsqrsumo1  20294  jensenlem2  20298  amgm  20301  logdifbnd  20304  harmonicbnd4  20320  fsumharmonic  20321  ftalem1  20326  ftalem5  20330  basellem1  20334  basellem8  20341  ppip1le  20415  ppiltx  20431  sqff1o  20436  chtublem  20466  chpub  20475  logfaclbnd  20477  logfacrlim  20479  logexprlim  20480  mersenne  20482  bcmono  20532  bcmax  20533  bposlem2  20540  bposlem5  20543  lgslem3  20553  lgsquadlem1  20609  lgsquadlem2  20610  2sqblem  20632  chebbnd1  20637  chtppilimlem1  20638  chto1ub  20641  chpchtlim  20644  chpo1ubb  20646  rplogsumlem1  20649  rplogsumlem2  20650  rpvmasumlem  20652  dchrisumlem1  20654  dchrisumlem2  20655  dchrmusum2  20659  dchrvmasumlem2  20663  dchrvmasumlem3  20664  dchrvmasumiflem1  20666  dchrisum0flblem1  20673  dchrisum0fno1  20676  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  rplogsum  20692  mudivsum  20695  mulogsumlem  20696  mulog2sumlem1  20699  mulog2sumlem2  20700  vmalogdivsum2  20703  2vmadivsumlem  20705  selberglem2  20711  selberg2b  20717  logdivbnd  20721  selberg3lem1  20722  selberg3lem2  20723  selberg4lem1  20725  pntrmax  20729  pntrsumo1  20730  pntrlog2bndlem1  20742  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntrlog2bnd  20749  pntpbnd1a  20750  pntpbnd2  20752  pntibndlem2  20756  pntlemb  20762  pntlemg  20763  pntlemh  20764  pntlemr  20767  pntlemj  20768  pntlemf  20770  pntlemo  20772  pnt  20779  padicabv  20795  ostth2lem2  20799  ostth2lem3  20800  ostth3  20803  nvmtri2  21254  nvabs  21255  nvge0  21256  nvlmle  21281  smcnlem  21286  nmblolbii  21393  blocnilem  21398  siii  21447  ubthlem2  21466  minvecolem3  21471  htthlem  21513  bcsiALT  21774  bcs3  21778  chscllem4  22235  0cnop  22575  0cnfn  22576  nmbdoplbi  22620  nmcoplbi  22624  nmophmi  22627  nmbdfnlbi  22645  nmcfnlbi  22648  nlelchi  22657  riesz1  22661  cnlnadjlem2  22664  nmopadjlei  22684  nmoptrii  22690  nmopcoi  22691  nmopcoadji  22697  unierri  22700  branmfn  22701  pjs14i  22806  hstle  22826  cdj3lem2b  23033  ltesubnnd  23049  ballotlemsel1i  23087  ballotlemro  23097  xlt2addrd  23268  eliccelico  23285  elicoelioo  23286  sqsscirc1  23307  tpr2rico  23311  esumcst  23451  esumpcvgval  23461  measiun  23560  dya2iocct  23596  erdsze2lem1  23749  sinccvglem  24020  faclimlem5  24121  prodfclim1  24167  nodense  24414  nobnddown  24426  brbtwn2  24605  colinearalglem4  24609  supadd  24996  ltflcei  24998  lxflflp1  25000  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  ibladdnclem  25007  ftc1cnnclem  25024  ftc1cnnc  25025  mslb1  25710  msra3  25712  fnemeet1  26418  trirn  26566  geomcau  26578  prdsbnd  26620  cntotbnd  26623  heiborlem4  26641  rrndstprj2  26658  rrncmslem  26659  rrnequiv  26662  iccbnd  26667  lzenom  26952  icodiamlt  27008  irrapxlem2  27011  irrapxlem3  27012  irrapxlem5  27014  pellexlem2  27018  pell14qrgt0  27047  pellfundlb  27072  pellfundex  27074  pellfund14  27086  rmspecsqrnq  27094  jm2.24nn  27149  jm2.17a  27150  jm2.17b  27151  congabseq  27164  acongrep  27170  acongeq  27173  jm2.26lem3  27197  jm2.27a  27201  jm2.27c  27203  hbtlem2  27431  dgraaub  27456  f1otrspeq  27493  pmtrfrn  27503  pmtrfconj  27510  symggen  27514  psgnunilem4  27523  idomodle  27615  fmul01  27813  fmul01lt1lem1  27817  fmul01lt1lem2  27818  climrec  27832  climsuse  27837  stoweidlem1  27853  stoweidlem3  27855  stoweidlem11  27863  stoweidlem13  27865  stoweidlem14  27866  stoweidlem16  27868  stoweidlem21  27873  stoweidlem25  27877  stoweidlem26  27878  stoweidlem36  27888  stoweidlem38  27890  stoweidlem41  27893  stoweidlem42  27894  stoweidlem45  27897  stoweidlem48  27900  stoweidlem51  27903  stoweidlem52  27904  stoweidlem62  27914  wallispilem3  27919  stirlinglem1  27926  stirlinglem5  27930  stirlinglem6  27931  stirlinglem7  27932  stirlinglem10  27935  stirlinglem12  27937  stirlinglem15  27940  cvlcvr1  30151  cvrat3  30253  dalem25  30509  cdlema1N  30602  dalawlem3  30684  dalawlem4  30685  dalawlem5  30686  dalawlem6  30687  dalawlem7  30688  dalawlem9  30690  dalawlem11  30692  dalawlem12  30693  lhp2lt  30812  lhpmcvr  30834  4atexlemcnd  30883  lautj  30904  trlle  30995  trlval3  30998  trlval4  30999  cdleme0moN  31036  cdleme13  31083  cdleme15  31089  cdleme19b  31115  cdleme20e  31124  cdleme20j  31129  cdleme22e  31155  cdleme22eALTN  31156  cdleme26fALTN  31173  cdleme26f  31174  cdleme27N  31180  cdleme41sn3a  31244  cdleme46fsvlpq  31316  cdlemeg46vrg  31338  cdlemg4  31428  cdlemg7N  31437  cdlemg9a  31443  cdlemg11b  31453  cdlemg12a  31454  trljco  31551  tendoidcl  31580  tendococl  31583  tendopltp  31591  tendo0tp  31600  tendoicl  31607  cdlemi2  31630  cdlemk5a  31646  cdlemk5  31647  cdlemk12  31661  cdlemkole  31664  cdlemk14  31665  cdlemk12u  31683  cdlemk37  31725  cdlemk39s-id  31751  cdlemk49  31762  cdlemk39u1  31778  cdlemk39u  31779  dian0  31851  cdlemm10N  31930  cdlemn2  32007  cdlemn10  32018  dihord1  32030  dihord10  32035  dihmeetlem4preN  32118  dihmeetlem18N  32136  dihmeetlem20N  32138  dihjatc  32229  mapdcnvatN  32478
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator