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

Theorem eqbrtrd 4196
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 4186 . 2  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
41, 3mpbird 224 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   class class class wbr 4176
This theorem is referenced by:  eqbrtrrd  4198  somin2  5235  en1b  7138  domunsncan  7171  fodomfi  7348  hartogslem1  7471  wemaplem2  7476  infdifsn  7571  carddomi2  7817  cdaun  8012  cda1dif  8016  mapcdaen  8024  cdaxpdom  8029  cdafi  8030  cdainf  8032  carden  8386  alephsuc3  8415  fpwwe2lem6  8470  fpwwe2lem7  8471  inar1  8610  rankcf  8612  lbinfmle  9923  supmul  9936  rpnnen1lem3  10562  xrmin1  10725  xrmin2  10726  ifle  10743  qbtwnxr  10746  xltnegi  10762  xleadd1a  10792  xlt2add  10799  xlemul1a  10827  xov1plusxeqvd  11001  ceim1l  11193  quoremz  11195  quoremnn0ALT  11197  modlt  11217  seqf1olem1  11321  bernneq  11464  discr  11475  faclbnd2  11541  faclbnd4lem3  11545  hashun2  11616  hashfun  11659  sqrlem6  12012  sqrlem7  12013  rddif  12103  amgm2  12132  climconst  12296  rlimconst  12297  serclim0  12330  rlimcn1  12341  mulcn2  12348  reccn2  12349  o1mul  12367  o1rlimmul  12371  iserex  12409  climlec2  12411  iserge0  12413  climcau  12423  caucvgrlem  12425  caucvgr  12428  iseraltlem2  12435  iseraltlem3  12436  iseralt  12437  fsumabs  12539  o1fsum  12551  iserabs  12553  climfsum  12558  isumless  12584  climcndslem2  12589  divrcnv  12591  flo1  12593  supcvg  12594  georeclim  12608  geomulcvg  12612  cvgrat  12619  mertenslem1  12620  efcvgfsum  12647  eftlub  12669  eflegeo  12681  tanhlt1  12720  tanhbnd  12721  ef01bndlem  12744  sin01bnd  12745  cos01bnd  12746  cos01gt0  12751  ruclem2  12790  ruclem3  12791  ruclem9  12796  ruclem11  12798  ruclem12  12799  bitsfzolem  12905  bitsfzo  12906  bitsinv1lem  12912  sadcaddlem  12928  mulgcd  13005  eucalglt  13035  prmind2  13049  mulgcddvds  13063  isprm5  13071  divdenle  13100  nonsq  13110  pythagtriplem4  13152  pclem  13171  pcpremul  13176  pczdvds  13195  pcprmpw2  13214  qexpz  13229  prmreclem4  13246  prmreclem5  13247  4sqlem10  13274  ramtub  13339  ramub2  13341  natpropd  14132  catciso  14221  p0le  14431  acsdomd  14566  divsgrp  14954  oddvds2  15161  odcau  15197  pgpfi  15198  pgpssslw  15207  sylow3lem4  15223  efgred2  15344  frgp0  15351  odadd2  15423  oddvdssubg  15429  ablfac1c  15588  ablfac1eu  15590  pgpfaclem3  15600  isabvd  15867  abvsubtri  15882  cyggic  16812  en2top  17009  1stcrest  17473  2ndcrest  17474  hausmapdom  17520  ufilen  17919  xmetrtri2  18343  prdsxmetlem  18355  bl2in  18387  xblcntrps  18397  xblcntr  18398  ssblps  18409  ssbl  18410  blssps  18411  blss  18412  blcld  18492  methaus  18507  metustexhalfOLD  18550  metustexhalf  18551  nrginvrcnlem  18683  nrginvrcn  18684  nmoi  18719  nmo0  18726  nmoid  18733  blcvx  18786  reperflem  18806  reconnlem2  18815  metdcnlem  18824  metdscn  18843  metnrmlem3  18848  mulc1cncf  18892  iccpnfhmeo  18927  cnheiborlem  18936  cnheibor  18937  lebnumii  18948  pcopt  19004  pcopt2  19005  pcoass  19006  nmoleub2lem  19079  nmoleub2lem3  19080  nmoleub2lem2  19081  ipcau2  19148  tchcphlem1  19149  minveclem3  19287  ivthlem2  19306  ivthlem3  19307  ivth2  19309  ovollb  19332  ovolsslem  19337  ovollb2lem  19341  ovolctb  19343  ovoliunlem1  19355  ovolsca  19368  ovolicc1  19369  ovolicc2lem4  19373  nulmbl  19387  ioombl1lem4  19412  uniioovol  19428  uniioombllem3a  19433  uniioombllem4  19435  opnmbllem  19450  volcn  19455  volivth  19456  i1fadd  19544  i1fmul  19545  mbfi1fseqlem4  19567  mbfi1fseqlem5  19568  mbfi1fseqlem6  19569  itg2const2  19590  itg2seq  19591  itg2uba  19592  itg2split  19598  itg2monolem1  19599  itg2monolem3  19601  itg2i1fseq2  19605  itg2addlem  19607  itg2gt0  19609  itg2cnlem1  19610  itg2cnlem2  19611  itgless  19665  ibladdlem  19668  bddmulibl  19687  dveflem  19820  dvferm1lem  19825  dvferm2lem  19827  dvlip  19834  dvlipcn  19835  dvlip2  19836  dvle  19848  dvivthlem1  19849  lhop1lem  19854  dvcvx  19861  dvfsumabs  19864  dvfsumlem2  19868  dvfsumlem4  19870  dvfsumrlim2  19873  dvfsum2  19875  ftc1a  19878  ftc1lem4  19880  ftc1lem5  19881  deg1sub  19988  ply1divex  20016  deg1submon1p  20032  r1pdeglt  20038  dvdsq1p  20040  fta1glem2  20046  fta1g  20047  plyeq0lem  20086  dgrlt  20141  fta1lem  20181  aalioulem2  20207  aalioulem3  20208  aalioulem4  20209  aaliou3lem2  20217  aaliou3lem9  20224  taylply2  20241  ulmbdd  20271  ulmdvlem1  20273  mtest  20277  mtestbdd  20278  radcnvlem1  20286  radcnvle  20293  pserulm  20295  psercn  20299  pserdvlem2  20301  abelthlem2  20305  abelthlem5  20308  abelthlem7  20311  abelthlem8  20312  abelthlem9  20313  reeff1olem  20319  tangtx  20370  tanord  20397  efif1olem4  20404  logrnaddcl  20429  logcj  20458  logimul  20466  logneg2  20467  logdivlti  20472  divlogrlim  20483  logcnlem3  20492  logcnlem4  20493  efopn  20506  logtayllem  20507  logtayl  20508  cxpcn3lem  20588  cxpaddle  20593  abscxpbnd  20594  asinlem3  20668  asinneg  20683  asinsin  20689  atanlogaddlem  20710  atantan  20720  bndatandm  20726  atans2  20728  atantayl  20734  atantayl2  20735  atantayl3  20736  leibpi  20739  birthdaylem3  20749  rlimcnp  20761  efrlim  20765  cxplim  20767  cxp2lim  20772  cxploglim2  20774  divsqrsumo1  20779  jensenlem2  20783  amgm  20786  logdifbnd  20789  harmonicbnd4  20806  fsumharmonic  20807  ftalem1  20812  ftalem5  20816  basellem1  20820  basellem8  20827  ppip1le  20901  ppiltx  20917  sqff1o  20922  chtublem  20952  chpub  20961  logfaclbnd  20963  logfacrlim  20965  logexprlim  20966  mersenne  20968  bcmono  21018  bcmax  21019  bposlem2  21026  bposlem5  21029  lgslem3  21039  lgsquadlem1  21095  lgsquadlem2  21096  2sqblem  21118  chebbnd1  21123  chtppilimlem1  21124  chto1ub  21127  chpchtlim  21130  chpo1ubb  21132  rplogsumlem1  21135  rplogsumlem2  21136  rpvmasumlem  21138  dchrisumlem1  21140  dchrisumlem2  21141  dchrmusum2  21145  dchrvmasumlem2  21149  dchrvmasumlem3  21150  dchrvmasumiflem1  21152  dchrisum0flblem1  21159  dchrisum0fno1  21162  dchrisum0lem1b  21166  dchrisum0lem1  21167  dchrisum0lem2a  21168  dchrisum0lem2  21169  rplogsum  21178  mudivsum  21181  mulogsumlem  21182  mulog2sumlem1  21185  mulog2sumlem2  21186  vmalogdivsum2  21189  2vmadivsumlem  21191  selberglem2  21197  selberg2b  21203  logdivbnd  21207  selberg3lem1  21208  selberg3lem2  21209  selberg4lem1  21211  pntrmax  21215  pntrsumo1  21216  pntrlog2bndlem1  21228  pntrlog2bndlem2  21229  pntrlog2bndlem3  21230  pntrlog2bndlem4  21231  pntrlog2bndlem5  21232  pntrlog2bnd  21235  pntpbnd1a  21236  pntpbnd2  21238  pntibndlem2  21242  pntlemb  21248  pntlemg  21249  pntlemh  21250  pntlemr  21253  pntlemj  21254  pntlemf  21256  pntlemo  21258  pnt  21265  padicabv  21281  ostth2lem2  21285  ostth2lem3  21286  ostth3  21289  nvmtri2  22118  nvabs  22119  nvge0  22120  nvlmle  22145  smcnlem  22150  nmblolbii  22257  blocnilem  22262  siii  22311  ubthlem2  22330  minvecolem3  22335  htthlem  22377  bcsiALT  22638  bcs3  22642  chscllem4  23099  0cnop  23439  0cnfn  23440  nmbdoplbi  23484  nmcoplbi  23488  nmophmi  23491  nmbdfnlbi  23509  nmcfnlbi  23512  nlelchi  23521  riesz1  23525  cnlnadjlem2  23528  nmopadjlei  23548  nmoptrii  23554  nmopcoi  23555  nmopcoadji  23561  unierri  23564  branmfn  23565  pjs14i  23670  hstle  23690  cdj3lem2b  23897  xlt2addrd  24081  eliccelico  24097  elicoelioo  24098  ltesubnnd  24119  sqsscirc1  24263  tpr2rico  24267  esumcst  24412  measunl  24527  measiun  24529  ballotlemsel1i  24727  ballotlemro  24737  lgamgulmlem2  24771  lgamgulmlem3  24772  lgamgulmlem5  24774  lgambdd  24778  lgamcvg2  24796  erdsze2lem1  24846  sinccvglem  25066  divcnvlin  25169  prodfclim1  25178  iprodefisum  25275  faclimlem2  25315  nodense  25561  nobnddown  25573  brbtwn2  25752  colinearalglem4  25756  supadd  26142  ltflcei  26144  lxflflp1  26146  mblfinlem  26147  mblfinlem2  26148  ismblfin  26150  itg2addnclem  26159  itg2addnclem2  26160  itg2addnclem3  26161  itg2addnc  26162  ibladdnclem  26164  ftc1cnnclem  26181  ftc1cnnc  26182  fnemeet1  26289  trirn  26351  geomcau  26359  prdsbnd  26396  cntotbnd  26399  heiborlem4  26417  rrndstprj2  26434  rrncmslem  26435  rrnequiv  26438  iccbnd  26443  lzenom  26722  icodiamlt  26777  irrapxlem2  26780  irrapxlem3  26781  irrapxlem5  26783  pellexlem2  26787  pell14qrgt0  26816  pellfundlb  26841  pellfundex  26843  pellfund14  26855  rmspecsqrnq  26863  jm2.24nn  26918  jm2.17a  26919  jm2.17b  26920  congabseq  26933  acongrep  26939  acongeq  26942  jm2.26lem3  26966  jm2.27a  26970  jm2.27c  26972  hbtlem2  27200  dgraaub  27225  f1otrspeq  27262  pmtrfrn  27272  pmtrfconj  27279  symggen  27283  psgnunilem4  27292  idomodle  27384  fmul01  27581  fmul01lt1lem1  27585  fmul01lt1lem2  27586  climrec  27600  climsuse  27605  stoweidlem1  27621  stoweidlem11  27631  stoweidlem13  27633  stoweidlem14  27634  stoweidlem16  27636  stoweidlem21  27641  stoweidlem25  27645  stoweidlem26  27646  stoweidlem36  27656  stoweidlem38  27658  stoweidlem41  27661  stoweidlem42  27662  stoweidlem45  27665  stoweidlem48  27668  stoweidlem52  27672  stoweidlem62  27682  wallispilem3  27687  stirlinglem5  27698  stirlinglem6  27699  stirlinglem7  27700  stirlinglem10  27703  stirlinglem12  27705  stirlinglem15  27708  cvlcvr1  29826  cvrat3  29928  dalem25  30184  cdlema1N  30277  dalawlem3  30359  dalawlem4  30360  dalawlem5  30361  dalawlem6  30362  dalawlem7  30363  dalawlem9  30365  dalawlem11  30367  dalawlem12  30368  lhp2lt  30487  lhpmcvr  30509  4atexlemcnd  30558  lautj  30579  trlle  30670  trlval3  30673  trlval4  30674  cdleme0moN  30711  cdleme13  30758  cdleme15  30764  cdleme19b  30790  cdleme20e  30799  cdleme20j  30804  cdleme22e  30830  cdleme22eALTN  30831  cdleme26fALTN  30848  cdleme26f  30849  cdleme27N  30855  cdleme41sn3a  30919  cdleme46fsvlpq  30991  cdlemeg46vrg  31013  cdlemg4  31103  cdlemg7N  31112  cdlemg9a  31118  cdlemg11b  31128  cdlemg12a  31129  trljco  31226  tendoidcl  31255  tendococl  31258  tendopltp  31266  tendo0tp  31275  tendoicl  31282  cdlemi2  31305  cdlemk5a  31321  cdlemk5  31322  cdlemk12  31336  cdlemkole  31339  cdlemk14  31340  cdlemk12u  31358  cdlemk37  31400  cdlemk39s-id  31426  cdlemk49  31437  cdlemk39u1  31453  cdlemk39u  31454  dian0  31526  cdlemm10N  31605  cdlemn2  31682  cdlemn10  31693  dihord1  31705  dihord10  31710  dihmeetlem4preN  31793  dihmeetlem18N  31811  dihmeetlem20N  31813  dihjatc  31904  mapdcnvatN  32153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-br 4177
  Copyright terms: Public domain W3C validator