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

Theorem eqbrtrd 4232
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 4222 . 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 1652   class class class wbr 4212
This theorem is referenced by:  eqbrtrrd  4234  somin2  5272  en1b  7175  domunsncan  7208  fodomfi  7385  hartogslem1  7511  wemaplem2  7516  infdifsn  7611  carddomi2  7857  cdaun  8052  cda1dif  8056  mapcdaen  8064  cdaxpdom  8069  cdafi  8070  cdainf  8072  carden  8426  alephsuc3  8455  fpwwe2lem6  8510  fpwwe2lem7  8511  inar1  8650  rankcf  8652  lbinfmle  9963  supmul  9976  rpnnen1lem3  10602  xrmin1  10765  xrmin2  10766  ifle  10783  qbtwnxr  10786  xltnegi  10802  xleadd1a  10832  xlt2add  10839  xlemul1a  10867  xov1plusxeqvd  11041  ceim1l  11234  quoremz  11236  quoremnn0ALT  11238  modlt  11258  seqf1olem1  11362  bernneq  11505  discr  11516  faclbnd2  11582  faclbnd4lem3  11586  hashun2  11657  hashfun  11700  sqrlem6  12053  sqrlem7  12054  rddif  12144  amgm2  12173  climconst  12337  rlimconst  12338  serclim0  12371  rlimcn1  12382  mulcn2  12389  reccn2  12390  o1mul  12408  o1rlimmul  12412  iserex  12450  climlec2  12452  iserge0  12454  climcau  12464  caucvgrlem  12466  caucvgr  12469  iseraltlem2  12476  iseraltlem3  12477  iseralt  12478  fsumabs  12580  o1fsum  12592  iserabs  12594  climfsum  12599  isumless  12625  climcndslem2  12630  divrcnv  12632  flo1  12634  supcvg  12635  georeclim  12649  geomulcvg  12653  cvgrat  12660  mertenslem1  12661  efcvgfsum  12688  eftlub  12710  eflegeo  12722  tanhlt1  12761  tanhbnd  12762  ef01bndlem  12785  sin01bnd  12786  cos01bnd  12787  cos01gt0  12792  ruclem2  12831  ruclem3  12832  ruclem9  12837  ruclem11  12839  ruclem12  12840  bitsfzolem  12946  bitsfzo  12947  bitsinv1lem  12953  sadcaddlem  12969  mulgcd  13046  eucalglt  13076  prmind2  13090  mulgcddvds  13104  isprm5  13112  divdenle  13141  nonsq  13151  pythagtriplem4  13193  pclem  13212  pcpremul  13217  pczdvds  13236  pcprmpw2  13255  qexpz  13270  prmreclem4  13287  prmreclem5  13288  4sqlem10  13315  ramtub  13380  ramub2  13382  natpropd  14173  catciso  14262  p0le  14472  acsdomd  14607  divsgrp  14995  oddvds2  15202  odcau  15238  pgpfi  15239  pgpssslw  15248  sylow3lem4  15264  efgred2  15385  frgp0  15392  odadd2  15464  oddvdssubg  15470  ablfac1c  15629  ablfac1eu  15631  pgpfaclem3  15641  isabvd  15908  abvsubtri  15923  cyggic  16853  en2top  17050  1stcrest  17516  2ndcrest  17517  hausmapdom  17563  ufilen  17962  xmetrtri2  18386  prdsxmetlem  18398  bl2in  18430  xblcntrps  18440  xblcntr  18441  ssblps  18452  ssbl  18453  blssps  18454  blss  18455  blcld  18535  methaus  18550  metustexhalfOLD  18593  metustexhalf  18594  nrginvrcnlem  18726  nrginvrcn  18727  nmoi  18762  nmo0  18769  nmoid  18776  blcvx  18829  reperflem  18849  reconnlem2  18858  metdcnlem  18867  metdscn  18886  metnrmlem3  18891  mulc1cncf  18935  iccpnfhmeo  18970  cnheiborlem  18979  cnheibor  18980  lebnumii  18991  pcopt  19047  pcopt2  19048  pcoass  19049  nmoleub2lem  19122  nmoleub2lem3  19123  nmoleub2lem2  19124  ipcau2  19191  tchcphlem1  19192  minveclem3  19330  ivthlem2  19349  ivthlem3  19350  ivth2  19352  ovollb  19375  ovolsslem  19380  ovollb2lem  19384  ovolctb  19386  ovoliunlem1  19398  ovolsca  19411  ovolicc1  19412  ovolicc2lem4  19416  nulmbl  19430  ioombl1lem4  19455  uniioovol  19471  uniioombllem3a  19476  uniioombllem4  19478  opnmbllem  19493  volcn  19498  volivth  19499  i1fadd  19587  i1fmul  19588  mbfi1fseqlem4  19610  mbfi1fseqlem5  19611  mbfi1fseqlem6  19612  itg2const2  19633  itg2seq  19634  itg2uba  19635  itg2split  19641  itg2monolem1  19642  itg2monolem3  19644  itg2i1fseq2  19648  itg2addlem  19650  itg2gt0  19652  itg2cnlem1  19653  itg2cnlem2  19654  itgless  19708  ibladdlem  19711  bddmulibl  19730  dveflem  19863  dvferm1lem  19868  dvferm2lem  19870  dvlip  19877  dvlipcn  19878  dvlip2  19879  dvle  19891  dvivthlem1  19892  lhop1lem  19897  dvcvx  19904  dvfsumabs  19907  dvfsumlem2  19911  dvfsumlem4  19913  dvfsumrlim2  19916  dvfsum2  19918  ftc1a  19921  ftc1lem4  19923  ftc1lem5  19924  deg1sub  20031  ply1divex  20059  deg1submon1p  20075  r1pdeglt  20081  dvdsq1p  20083  fta1glem2  20089  fta1g  20090  plyeq0lem  20129  dgrlt  20184  fta1lem  20224  aalioulem2  20250  aalioulem3  20251  aalioulem4  20252  aaliou3lem2  20260  aaliou3lem9  20267  taylply2  20284  ulmbdd  20314  ulmdvlem1  20316  mtest  20320  mtestbdd  20321  radcnvlem1  20329  radcnvle  20336  pserulm  20338  psercn  20342  pserdvlem2  20344  abelthlem2  20348  abelthlem5  20351  abelthlem7  20354  abelthlem8  20355  abelthlem9  20356  reeff1olem  20362  tangtx  20413  tanord  20440  efif1olem4  20447  logrnaddcl  20472  logcj  20501  logimul  20509  logneg2  20510  logdivlti  20515  divlogrlim  20526  logcnlem3  20535  logcnlem4  20536  efopn  20549  logtayllem  20550  logtayl  20551  cxpcn3lem  20631  cxpaddle  20636  abscxpbnd  20637  asinlem3  20711  asinneg  20726  asinsin  20732  atanlogaddlem  20753  atantan  20763  bndatandm  20769  atans2  20771  atantayl  20777  atantayl2  20778  atantayl3  20779  leibpi  20782  birthdaylem3  20792  rlimcnp  20804  efrlim  20808  cxplim  20810  cxp2lim  20815  cxploglim2  20817  divsqrsumo1  20822  jensenlem2  20826  amgm  20829  logdifbnd  20832  harmonicbnd4  20849  fsumharmonic  20850  ftalem1  20855  ftalem5  20859  basellem1  20863  basellem8  20870  ppip1le  20944  ppiltx  20960  sqff1o  20965  chtublem  20995  chpub  21004  logfaclbnd  21006  logfacrlim  21008  logexprlim  21009  mersenne  21011  bcmono  21061  bcmax  21062  bposlem2  21069  bposlem5  21072  lgslem3  21082  lgsquadlem1  21138  lgsquadlem2  21139  2sqblem  21161  chebbnd1  21166  chtppilimlem1  21167  chto1ub  21170  chpchtlim  21173  chpo1ubb  21175  rplogsumlem1  21178  rplogsumlem2  21179  rpvmasumlem  21181  dchrisumlem1  21183  dchrisumlem2  21184  dchrmusum2  21188  dchrvmasumlem2  21192  dchrvmasumlem3  21193  dchrvmasumiflem1  21195  dchrisum0flblem1  21202  dchrisum0fno1  21205  dchrisum0lem1b  21209  dchrisum0lem1  21210  dchrisum0lem2a  21211  dchrisum0lem2  21212  rplogsum  21221  mudivsum  21224  mulogsumlem  21225  mulog2sumlem1  21228  mulog2sumlem2  21229  vmalogdivsum2  21232  2vmadivsumlem  21234  selberglem2  21240  selberg2b  21246  logdivbnd  21250  selberg3lem1  21251  selberg3lem2  21252  selberg4lem1  21254  pntrmax  21258  pntrsumo1  21259  pntrlog2bndlem1  21271  pntrlog2bndlem2  21272  pntrlog2bndlem3  21273  pntrlog2bndlem4  21274  pntrlog2bndlem5  21275  pntrlog2bnd  21278  pntpbnd1a  21279  pntpbnd2  21281  pntibndlem2  21285  pntlemb  21291  pntlemg  21292  pntlemh  21293  pntlemr  21296  pntlemj  21297  pntlemf  21299  pntlemo  21301  pnt  21308  padicabv  21324  ostth2lem2  21328  ostth2lem3  21329  ostth3  21332  nvmtri2  22161  nvabs  22162  nvge0  22163  nvlmle  22188  smcnlem  22193  nmblolbii  22300  blocnilem  22305  siii  22354  ubthlem2  22373  minvecolem3  22378  htthlem  22420  bcsiALT  22681  bcs3  22685  chscllem4  23142  0cnop  23482  0cnfn  23483  nmbdoplbi  23527  nmcoplbi  23531  nmophmi  23534  nmbdfnlbi  23552  nmcfnlbi  23555  nlelchi  23564  riesz1  23568  cnlnadjlem2  23571  nmopadjlei  23591  nmoptrii  23597  nmopcoi  23598  nmopcoadji  23604  unierri  23607  branmfn  23608  pjs14i  23713  hstle  23733  cdj3lem2b  23940  xlt2addrd  24124  eliccelico  24140  elicoelioo  24141  ltesubnnd  24162  sqsscirc1  24306  tpr2rico  24310  esumcst  24455  measunl  24570  measiun  24572  ballotlemsel1i  24770  ballotlemro  24780  lgamgulmlem2  24814  lgamgulmlem3  24815  lgamgulmlem5  24817  lgambdd  24821  lgamcvg2  24839  erdsze2lem1  24889  sinccvglem  25109  divcnvlin  25212  prodfclim1  25221  iprodefisum  25318  faclimlem2  25363  nodense  25644  nobnddown  25656  brbtwn2  25844  colinearalglem4  25848  supadd  26238  ltflcei  26239  lxflflp1  26241  opnmbllem0  26242  mblfinlem2  26244  mblfinlem3  26245  ismblfin  26247  itg2addnclem  26256  itg2addnclem2  26257  itg2addnclem3  26258  itg2addnc  26259  ibladdnclem  26261  ftc1cnnclem  26278  ftc1cnnc  26279  ftc1anc  26288  fnemeet1  26395  trirn  26457  geomcau  26465  prdsbnd  26502  cntotbnd  26505  heiborlem4  26523  rrndstprj2  26540  rrncmslem  26541  rrnequiv  26544  iccbnd  26549  lzenom  26828  icodiamlt  26883  irrapxlem2  26886  irrapxlem3  26887  irrapxlem5  26889  pellexlem2  26893  pell14qrgt0  26922  pellfundlb  26947  pellfundex  26949  pellfund14  26961  rmspecsqrnq  26969  jm2.24nn  27024  jm2.17a  27025  jm2.17b  27026  congabseq  27039  acongrep  27045  acongeq  27048  jm2.26lem3  27072  jm2.27a  27076  jm2.27c  27078  hbtlem2  27305  dgraaub  27330  f1otrspeq  27367  pmtrfrn  27377  pmtrfconj  27384  symggen  27388  psgnunilem4  27397  idomodle  27489  fmul01  27686  fmul01lt1lem1  27690  fmul01lt1lem2  27691  climrec  27705  climsuse  27710  stoweidlem1  27726  stoweidlem11  27736  stoweidlem13  27738  stoweidlem14  27739  stoweidlem16  27741  stoweidlem21  27746  stoweidlem25  27750  stoweidlem26  27751  stoweidlem36  27761  stoweidlem38  27763  stoweidlem41  27766  stoweidlem42  27767  stoweidlem45  27770  stoweidlem48  27773  stoweidlem52  27777  stoweidlem62  27787  wallispilem3  27792  stirlinglem5  27803  stirlinglem6  27804  stirlinglem7  27805  stirlinglem10  27808  stirlinglem12  27810  stirlinglem15  27813  ccatsymb  28179  2cshw2lem1  28252  2cshwid  28258  cshweqdif2  28270  cvlcvr1  30137  cvrat3  30239  dalem25  30495  cdlema1N  30588  dalawlem3  30670  dalawlem4  30671  dalawlem5  30672  dalawlem6  30673  dalawlem7  30674  dalawlem9  30676  dalawlem11  30678  dalawlem12  30679  lhp2lt  30798  lhpmcvr  30820  4atexlemcnd  30869  lautj  30890  trlle  30981  trlval3  30984  trlval4  30985  cdleme0moN  31022  cdleme13  31069  cdleme15  31075  cdleme19b  31101  cdleme20e  31110  cdleme20j  31115  cdleme22e  31141  cdleme22eALTN  31142  cdleme26fALTN  31159  cdleme26f  31160  cdleme27N  31166  cdleme41sn3a  31230  cdleme46fsvlpq  31302  cdlemeg46vrg  31324  cdlemg4  31414  cdlemg7N  31423  cdlemg9a  31429  cdlemg11b  31439  cdlemg12a  31440  trljco  31537  tendoidcl  31566  tendococl  31569  tendopltp  31577  tendo0tp  31586  tendoicl  31593  cdlemi2  31616  cdlemk5a  31632  cdlemk5  31633  cdlemk12  31647  cdlemkole  31650  cdlemk14  31651  cdlemk12u  31669  cdlemk37  31711  cdlemk39s-id  31737  cdlemk49  31748  cdlemk39u1  31764  cdlemk39u  31765  dian0  31837  cdlemm10N  31916  cdlemn2  31993  cdlemn10  32004  dihord1  32016  dihord10  32021  dihmeetlem4preN  32104  dihmeetlem18N  32122  dihmeetlem20N  32124  dihjatc  32215  mapdcnvatN  32464
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator