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

Theorem eqbrtrd 4145
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 4135 . 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 1647   class class class wbr 4125
This theorem is referenced by:  eqbrtrrd  4147  somin2  5184  en1b  7072  domunsncan  7105  fodomfi  7282  hartogslem1  7404  wemaplem2  7409  infdifsn  7504  carddomi2  7750  cdaun  7945  cda1dif  7949  mapcdaen  7957  cdaxpdom  7962  cdafi  7963  cdainf  7965  carden  8320  alephsuc3  8349  fpwwe2lem6  8404  fpwwe2lem7  8405  inar1  8544  rankcf  8546  lbinfmle  9856  supmul  9869  rpnnen1lem3  10495  xrmin1  10658  xrmin2  10659  ifle  10676  qbtwnxr  10679  xltnegi  10695  xleadd1a  10725  xlt2add  10732  xlemul1a  10760  xov1plusxeqvd  10933  ceim1l  11121  quoremz  11123  quoremnn0ALT  11125  modlt  11145  seqf1olem1  11249  bernneq  11392  discr  11403  faclbnd2  11469  faclbnd4lem3  11473  hashun2  11544  hashfun  11587  sqrlem6  11940  sqrlem7  11941  rddif  12031  amgm2  12060  climconst  12224  rlimconst  12225  serclim0  12258  rlimcn1  12269  mulcn2  12276  reccn2  12277  o1mul  12295  o1rlimmul  12299  iserex  12337  climlec2  12339  iserge0  12341  climcau  12351  caucvgrlem  12353  caucvgr  12356  iseraltlem2  12363  iseraltlem3  12364  iseralt  12365  fsumabs  12467  o1fsum  12479  iserabs  12481  climfsum  12486  isumless  12512  climcndslem2  12517  divrcnv  12519  flo1  12521  supcvg  12522  georeclim  12536  geomulcvg  12540  cvgrat  12547  mertenslem1  12548  efcvgfsum  12575  eftlub  12597  eflegeo  12609  tanhlt1  12648  tanhbnd  12649  ef01bndlem  12672  sin01bnd  12673  cos01bnd  12674  cos01gt0  12679  ruclem2  12718  ruclem3  12719  ruclem9  12724  ruclem11  12726  ruclem12  12727  bitsfzolem  12833  bitsfzo  12834  bitsinv1lem  12840  sadcaddlem  12856  mulgcd  12933  eucalglt  12963  prmind2  12977  mulgcddvds  12991  isprm5  12999  divdenle  13028  nonsq  13038  pythagtriplem4  13080  pclem  13099  pcpremul  13104  pczdvds  13123  pcprmpw2  13142  qexpz  13157  prmreclem4  13174  prmreclem5  13175  4sqlem10  13202  ramtub  13267  ramub2  13269  natpropd  14060  catciso  14149  p0le  14359  acsdomd  14494  divsgrp  14882  oddvds2  15089  odcau  15125  pgpfi  15126  pgpssslw  15135  sylow3lem4  15151  efgred2  15272  frgp0  15279  odadd2  15351  oddvdssubg  15357  ablfac1c  15516  ablfac1eu  15518  pgpfaclem3  15528  isabvd  15795  abvsubtri  15810  cyggic  16743  en2top  16940  1stcrest  17396  2ndcrest  17397  hausmapdom  17443  ufilen  17838  xmetrtri2  18133  prdsxmetlem  18145  bl2in  18170  xblcntr  18176  ssbl  18184  blss  18185  blcld  18264  methaus  18279  nrginvrcnlem  18414  nrginvrcn  18415  nmoi  18450  nmo0  18457  nmoid  18464  blcvx  18517  reperflem  18537  reconnlem2  18546  metdcnlem  18555  metdscn  18574  metnrmlem3  18579  mulc1cncf  18623  iccpnfhmeo  18658  cnheiborlem  18667  cnheibor  18668  lebnumii  18679  pcopt  18735  pcopt2  18736  pcoass  18737  nmoleub2lem  18810  nmoleub2lem3  18811  nmoleub2lem2  18812  ipcau2  18879  tchcphlem1  18880  minveclem3  19008  ivthlem2  19027  ivthlem3  19028  ivth2  19030  ovollb  19053  ovolsslem  19058  ovollb2lem  19062  ovolctb  19064  ovoliunlem1  19076  ovolsca  19089  ovolicc1  19090  ovolicc2lem4  19094  nulmbl  19108  ioombl1lem4  19133  uniioovol  19149  uniioombllem3a  19154  uniioombllem4  19156  opnmbllem  19171  volcn  19176  volivth  19177  i1fadd  19265  i1fmul  19266  mbfi1fseqlem4  19288  mbfi1fseqlem5  19289  mbfi1fseqlem6  19290  itg2const2  19311  itg2seq  19312  itg2uba  19313  itg2split  19319  itg2monolem1  19320  itg2monolem3  19322  itg2i1fseq2  19326  itg2addlem  19328  itg2gt0  19330  itg2cnlem1  19331  itg2cnlem2  19332  itgless  19386  ibladdlem  19389  bddmulibl  19408  dveflem  19541  dvferm1lem  19546  dvferm2lem  19548  dvlip  19555  dvlipcn  19556  dvlip2  19557  dvle  19569  dvivthlem1  19570  lhop1lem  19575  dvcvx  19582  dvfsumabs  19585  dvfsumlem2  19589  dvfsumlem4  19591  dvfsumrlim2  19594  dvfsum2  19596  ftc1a  19599  ftc1lem4  19601  ftc1lem5  19602  deg1sub  19709  ply1divex  19737  deg1submon1p  19753  r1pdeglt  19759  dvdsq1p  19761  fta1glem2  19767  fta1g  19768  plyeq0lem  19807  dgrlt  19862  fta1lem  19902  aalioulem2  19928  aalioulem3  19929  aalioulem4  19930  aaliou3lem2  19938  aaliou3lem9  19945  taylply2  19962  ulmbdd  19992  ulmdvlem1  19994  mtest  19998  mtestbdd  19999  radcnvlem1  20007  radcnvle  20014  pserulm  20016  psercn  20020  pserdvlem2  20022  abelthlem2  20026  abelthlem5  20029  abelthlem7  20032  abelthlem8  20033  abelthlem9  20034  reeff1olem  20040  tangtx  20091  tanord  20118  efif1olem4  20125  logrnaddcl  20150  logcj  20179  logimul  20187  logneg2  20188  logdivlti  20193  divlogrlim  20204  logcnlem3  20213  logcnlem4  20214  efopn  20227  logtayllem  20228  logtayl  20229  cxpcn3lem  20309  cxpaddle  20314  abscxpbnd  20315  asinlem3  20389  asinneg  20404  asinsin  20410  atanlogaddlem  20431  atantan  20441  bndatandm  20447  atans2  20449  atantayl  20455  atantayl2  20456  atantayl3  20457  leibpi  20460  birthdaylem3  20470  rlimcnp  20482  efrlim  20486  cxplim  20488  cxp2lim  20493  cxploglim2  20495  divsqrsumo1  20500  jensenlem2  20504  amgm  20507  logdifbnd  20510  harmonicbnd4  20527  fsumharmonic  20528  ftalem1  20533  ftalem5  20537  basellem1  20541  basellem8  20548  ppip1le  20622  ppiltx  20638  sqff1o  20643  chtublem  20673  chpub  20682  logfaclbnd  20684  logfacrlim  20686  logexprlim  20687  mersenne  20689  bcmono  20739  bcmax  20740  bposlem2  20747  bposlem5  20750  lgslem3  20760  lgsquadlem1  20816  lgsquadlem2  20817  2sqblem  20839  chebbnd1  20844  chtppilimlem1  20845  chto1ub  20848  chpchtlim  20851  chpo1ubb  20853  rplogsumlem1  20856  rplogsumlem2  20857  rpvmasumlem  20859  dchrisumlem1  20861  dchrisumlem2  20862  dchrmusum2  20866  dchrvmasumlem2  20870  dchrvmasumlem3  20871  dchrvmasumiflem1  20873  dchrisum0flblem1  20880  dchrisum0fno1  20883  dchrisum0lem1b  20887  dchrisum0lem1  20888  dchrisum0lem2a  20889  dchrisum0lem2  20890  rplogsum  20899  mudivsum  20902  mulogsumlem  20903  mulog2sumlem1  20906  mulog2sumlem2  20907  vmalogdivsum2  20910  2vmadivsumlem  20912  selberglem2  20918  selberg2b  20924  logdivbnd  20928  selberg3lem1  20929  selberg3lem2  20930  selberg4lem1  20932  pntrmax  20936  pntrsumo1  20937  pntrlog2bndlem1  20949  pntrlog2bndlem2  20950  pntrlog2bndlem3  20951  pntrlog2bndlem4  20952  pntrlog2bndlem5  20953  pntrlog2bnd  20956  pntpbnd1a  20957  pntpbnd2  20959  pntibndlem2  20963  pntlemb  20969  pntlemg  20970  pntlemh  20971  pntlemr  20974  pntlemj  20975  pntlemf  20977  pntlemo  20979  pnt  20986  padicabv  21002  ostth2lem2  21006  ostth2lem3  21007  ostth3  21010  nvmtri2  21672  nvabs  21673  nvge0  21674  nvlmle  21699  smcnlem  21704  nmblolbii  21811  blocnilem  21816  siii  21865  ubthlem2  21884  minvecolem3  21889  htthlem  21931  bcsiALT  22192  bcs3  22196  chscllem4  22653  0cnop  22993  0cnfn  22994  nmbdoplbi  23038  nmcoplbi  23042  nmophmi  23045  nmbdfnlbi  23063  nmcfnlbi  23066  nlelchi  23075  riesz1  23079  cnlnadjlem2  23082  nmopadjlei  23102  nmoptrii  23108  nmopcoi  23109  nmopcoadji  23115  unierri  23118  branmfn  23119  pjs14i  23224  hstle  23244  cdj3lem2b  23451  xlt2addrd  23645  eliccelico  23662  elicoelioo  23663  ltesubnnd  23686  sqsscirc1  23782  tpr2rico  23786  metustexhalf  23920  esumcst  24041  esumpcvgval  24054  measunl  24154  measiun  24156  ballotlemsel1i  24339  ballotlemro  24349  lgamgulmlem2  24383  lgamgulmlem3  24384  lgamgulmlem5  24386  lgambdd  24390  lgamcvg2  24408  erdsze2lem1  24458  sinccvglem  24677  divcnvlin  24781  prodfclim1  24790  faclimlem2  24923  nodense  25169  nobnddown  25181  brbtwn2  25360  colinearalglem4  25364  supadd  25751  ltflcei  25753  lxflflp1  25755  itg2addnclem  25760  itg2addnclem2  25761  itg2addnc  25762  ibladdnclem  25764  ftc1cnnclem  25781  ftc1cnnc  25782  fnemeet1  25907  trirn  26055  geomcau  26067  prdsbnd  26108  cntotbnd  26111  heiborlem4  26129  rrndstprj2  26146  rrncmslem  26147  rrnequiv  26150  iccbnd  26155  lzenom  26440  icodiamlt  26496  irrapxlem2  26499  irrapxlem3  26500  irrapxlem5  26502  pellexlem2  26506  pell14qrgt0  26535  pellfundlb  26560  pellfundex  26562  pellfund14  26574  rmspecsqrnq  26582  jm2.24nn  26637  jm2.17a  26638  jm2.17b  26639  congabseq  26652  acongrep  26658  acongeq  26661  jm2.26lem3  26685  jm2.27a  26689  jm2.27c  26691  hbtlem2  26919  dgraaub  26944  f1otrspeq  26981  pmtrfrn  26991  pmtrfconj  26998  symggen  27002  psgnunilem4  27011  idomodle  27103  fmul01  27301  fmul01lt1lem1  27305  fmul01lt1lem2  27306  climrec  27320  climsuse  27325  stoweidlem1  27341  stoweidlem3  27343  stoweidlem11  27351  stoweidlem13  27353  stoweidlem14  27354  stoweidlem16  27356  stoweidlem21  27361  stoweidlem25  27365  stoweidlem26  27366  stoweidlem36  27376  stoweidlem38  27378  stoweidlem41  27381  stoweidlem42  27382  stoweidlem45  27385  stoweidlem48  27388  stoweidlem51  27391  stoweidlem52  27392  stoweidlem62  27402  wallispilem3  27407  stirlinglem1  27414  stirlinglem5  27418  stirlinglem6  27419  stirlinglem7  27420  stirlinglem10  27423  stirlinglem12  27425  stirlinglem15  27428  cvlcvr1  29588  cvrat3  29690  dalem25  29946  cdlema1N  30039  dalawlem3  30121  dalawlem4  30122  dalawlem5  30123  dalawlem6  30124  dalawlem7  30125  dalawlem9  30127  dalawlem11  30129  dalawlem12  30130  lhp2lt  30249  lhpmcvr  30271  4atexlemcnd  30320  lautj  30341  trlle  30432  trlval3  30435  trlval4  30436  cdleme0moN  30473  cdleme13  30520  cdleme15  30526  cdleme19b  30552  cdleme20e  30561  cdleme20j  30566  cdleme22e  30592  cdleme22eALTN  30593  cdleme26fALTN  30610  cdleme26f  30611  cdleme27N  30617  cdleme41sn3a  30681  cdleme46fsvlpq  30753  cdlemeg46vrg  30775  cdlemg4  30865  cdlemg7N  30874  cdlemg9a  30880  cdlemg11b  30890  cdlemg12a  30891  trljco  30988  tendoidcl  31017  tendococl  31020  tendopltp  31028  tendo0tp  31037  tendoicl  31044  cdlemi2  31067  cdlemk5a  31083  cdlemk5  31084  cdlemk12  31098  cdlemkole  31101  cdlemk14  31102  cdlemk12u  31120  cdlemk37  31162  cdlemk39s-id  31188  cdlemk49  31199  cdlemk39u1  31215  cdlemk39u  31216  dian0  31288  cdlemm10N  31367  cdlemn2  31444  cdlemn10  31455  dihord1  31467  dihord10  31472  dihmeetlem4preN  31555  dihmeetlem18N  31573  dihmeetlem20N  31575  dihjatc  31666  mapdcnvatN  31915
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-br 4126
  Copyright terms: Public domain W3C validator