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

Theorem eqbrtrd 4233
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 4223 . 2  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
41, 3mpbird 225 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   class class class wbr 4213
This theorem is referenced by:  eqbrtrrd  4235  somin2  5273  en1b  7176  domunsncan  7209  fodomfi  7386  hartogslem1  7512  wemaplem2  7517  infdifsn  7612  carddomi2  7858  cdaun  8053  cda1dif  8057  mapcdaen  8065  cdaxpdom  8070  cdafi  8071  cdainf  8073  carden  8427  alephsuc3  8456  fpwwe2lem6  8511  fpwwe2lem7  8512  inar1  8651  rankcf  8653  lbinfmle  9964  supmul  9977  rpnnen1lem3  10603  xrmin1  10766  xrmin2  10767  ifle  10784  qbtwnxr  10787  xltnegi  10803  xleadd1a  10833  xlt2add  10840  xlemul1a  10868  xov1plusxeqvd  11042  ceim1l  11235  quoremz  11237  quoremnn0ALT  11239  modlt  11259  seqf1olem1  11363  bernneq  11506  discr  11517  faclbnd2  11583  faclbnd4lem3  11587  hashun2  11658  hashfun  11701  sqrlem6  12054  sqrlem7  12055  rddif  12145  amgm2  12174  climconst  12338  rlimconst  12339  serclim0  12372  rlimcn1  12383  mulcn2  12390  reccn2  12391  o1mul  12409  o1rlimmul  12413  iserex  12451  climlec2  12453  iserge0  12455  climcau  12465  caucvgrlem  12467  caucvgr  12470  iseraltlem2  12477  iseraltlem3  12478  iseralt  12479  fsumabs  12581  o1fsum  12593  iserabs  12595  climfsum  12600  isumless  12626  climcndslem2  12631  divrcnv  12633  flo1  12635  supcvg  12636  georeclim  12650  geomulcvg  12654  cvgrat  12661  mertenslem1  12662  efcvgfsum  12689  eftlub  12711  eflegeo  12723  tanhlt1  12762  tanhbnd  12763  ef01bndlem  12786  sin01bnd  12787  cos01bnd  12788  cos01gt0  12793  ruclem2  12832  ruclem3  12833  ruclem9  12838  ruclem11  12840  ruclem12  12841  bitsfzolem  12947  bitsfzo  12948  bitsinv1lem  12954  sadcaddlem  12970  mulgcd  13047  eucalglt  13077  prmind2  13091  mulgcddvds  13105  isprm5  13113  divdenle  13142  nonsq  13152  pythagtriplem4  13194  pclem  13213  pcpremul  13218  pczdvds  13237  pcprmpw2  13256  qexpz  13271  prmreclem4  13288  prmreclem5  13289  4sqlem10  13316  ramtub  13381  ramub2  13383  natpropd  14174  catciso  14263  p0le  14473  acsdomd  14608  divsgrp  14996  oddvds2  15203  odcau  15239  pgpfi  15240  pgpssslw  15249  sylow3lem4  15265  efgred2  15386  frgp0  15393  odadd2  15465  oddvdssubg  15471  ablfac1c  15630  ablfac1eu  15632  pgpfaclem3  15642  isabvd  15909  abvsubtri  15924  cyggic  16854  en2top  17051  1stcrest  17517  2ndcrest  17518  hausmapdom  17564  ufilen  17963  xmetrtri2  18387  prdsxmetlem  18399  bl2in  18431  xblcntrps  18441  xblcntr  18442  ssblps  18453  ssbl  18454  blssps  18455  blss  18456  blcld  18536  methaus  18551  metustexhalfOLD  18594  metustexhalf  18595  nrginvrcnlem  18727  nrginvrcn  18728  nmoi  18763  nmo0  18770  nmoid  18777  blcvx  18830  reperflem  18850  reconnlem2  18859  metdcnlem  18868  metdscn  18887  metnrmlem3  18892  mulc1cncf  18936  iccpnfhmeo  18971  cnheiborlem  18980  cnheibor  18981  lebnumii  18992  pcopt  19048  pcopt2  19049  pcoass  19050  nmoleub2lem  19123  nmoleub2lem3  19124  nmoleub2lem2  19125  ipcau2  19192  tchcphlem1  19193  minveclem3  19331  ivthlem2  19350  ivthlem3  19351  ivth2  19353  ovollb  19376  ovolsslem  19381  ovollb2lem  19385  ovolctb  19387  ovoliunlem1  19399  ovolsca  19412  ovolicc1  19413  ovolicc2lem4  19417  nulmbl  19431  ioombl1lem4  19456  uniioovol  19472  uniioombllem3a  19477  uniioombllem4  19479  opnmbllem  19494  volcn  19499  volivth  19500  i1fadd  19588  i1fmul  19589  mbfi1fseqlem4  19611  mbfi1fseqlem5  19612  mbfi1fseqlem6  19613  itg2const2  19634  itg2seq  19635  itg2uba  19636  itg2split  19642  itg2monolem1  19643  itg2monolem3  19645  itg2i1fseq2  19649  itg2addlem  19651  itg2gt0  19653  itg2cnlem1  19654  itg2cnlem2  19655  itgless  19709  ibladdlem  19712  bddmulibl  19731  dveflem  19864  dvferm1lem  19869  dvferm2lem  19871  dvlip  19878  dvlipcn  19879  dvlip2  19880  dvle  19892  dvivthlem1  19893  lhop1lem  19898  dvcvx  19905  dvfsumabs  19908  dvfsumlem2  19912  dvfsumlem4  19914  dvfsumrlim2  19917  dvfsum2  19919  ftc1a  19922  ftc1lem4  19924  ftc1lem5  19925  deg1sub  20032  ply1divex  20060  deg1submon1p  20076  r1pdeglt  20082  dvdsq1p  20084  fta1glem2  20090  fta1g  20091  plyeq0lem  20130  dgrlt  20185  fta1lem  20225  aalioulem2  20251  aalioulem3  20252  aalioulem4  20253  aaliou3lem2  20261  aaliou3lem9  20268  taylply2  20285  ulmbdd  20315  ulmdvlem1  20317  mtest  20321  mtestbdd  20322  radcnvlem1  20330  radcnvle  20337  pserulm  20339  psercn  20343  pserdvlem2  20345  abelthlem2  20349  abelthlem5  20352  abelthlem7  20355  abelthlem8  20356  abelthlem9  20357  reeff1olem  20363  tangtx  20414  tanord  20441  efif1olem4  20448  logrnaddcl  20473  logcj  20502  logimul  20510  logneg2  20511  logdivlti  20516  divlogrlim  20527  logcnlem3  20536  logcnlem4  20537  efopn  20550  logtayllem  20551  logtayl  20552  cxpcn3lem  20632  cxpaddle  20637  abscxpbnd  20638  asinlem3  20712  asinneg  20727  asinsin  20733  atanlogaddlem  20754  atantan  20764  bndatandm  20770  atans2  20772  atantayl  20778  atantayl2  20779  atantayl3  20780  leibpi  20783  birthdaylem3  20793  rlimcnp  20805  efrlim  20809  cxplim  20811  cxp2lim  20816  cxploglim2  20818  divsqrsumo1  20823  jensenlem2  20827  amgm  20830  logdifbnd  20833  harmonicbnd4  20850  fsumharmonic  20851  ftalem1  20856  ftalem5  20860  basellem1  20864  basellem8  20871  ppip1le  20945  ppiltx  20961  sqff1o  20966  chtublem  20996  chpub  21005  logfaclbnd  21007  logfacrlim  21009  logexprlim  21010  mersenne  21012  bcmono  21062  bcmax  21063  bposlem2  21070  bposlem5  21073  lgslem3  21083  lgsquadlem1  21139  lgsquadlem2  21140  2sqblem  21162  chebbnd1  21167  chtppilimlem1  21168  chto1ub  21171  chpchtlim  21174  chpo1ubb  21176  rplogsumlem1  21179  rplogsumlem2  21180  rpvmasumlem  21182  dchrisumlem1  21184  dchrisumlem2  21185  dchrmusum2  21189  dchrvmasumlem2  21193  dchrvmasumlem3  21194  dchrvmasumiflem1  21196  dchrisum0flblem1  21203  dchrisum0fno1  21206  dchrisum0lem1b  21210  dchrisum0lem1  21211  dchrisum0lem2a  21212  dchrisum0lem2  21213  rplogsum  21222  mudivsum  21225  mulogsumlem  21226  mulog2sumlem1  21229  mulog2sumlem2  21230  vmalogdivsum2  21233  2vmadivsumlem  21235  selberglem2  21241  selberg2b  21247  logdivbnd  21251  selberg3lem1  21252  selberg3lem2  21253  selberg4lem1  21255  pntrmax  21259  pntrsumo1  21260  pntrlog2bndlem1  21272  pntrlog2bndlem2  21273  pntrlog2bndlem3  21274  pntrlog2bndlem4  21275  pntrlog2bndlem5  21276  pntrlog2bnd  21279  pntpbnd1a  21280  pntpbnd2  21282  pntibndlem2  21286  pntlemb  21292  pntlemg  21293  pntlemh  21294  pntlemr  21297  pntlemj  21298  pntlemf  21300  pntlemo  21302  pnt  21309  padicabv  21325  ostth2lem2  21329  ostth2lem3  21330  ostth3  21333  nvmtri2  22162  nvabs  22163  nvge0  22164  nvlmle  22189  smcnlem  22194  nmblolbii  22301  blocnilem  22306  siii  22355  ubthlem2  22374  minvecolem3  22379  htthlem  22421  bcsiALT  22682  bcs3  22686  chscllem4  23143  0cnop  23483  0cnfn  23484  nmbdoplbi  23528  nmcoplbi  23532  nmophmi  23535  nmbdfnlbi  23553  nmcfnlbi  23556  nlelchi  23565  riesz1  23569  cnlnadjlem2  23572  nmopadjlei  23592  nmoptrii  23598  nmopcoi  23599  nmopcoadji  23605  unierri  23608  branmfn  23609  pjs14i  23714  hstle  23734  cdj3lem2b  23941  xlt2addrd  24125  eliccelico  24141  elicoelioo  24142  ltesubnnd  24163  sqsscirc1  24307  tpr2rico  24311  esumcst  24456  measunl  24571  measiun  24573  ballotlemsel1i  24771  ballotlemro  24781  lgamgulmlem2  24815  lgamgulmlem3  24816  lgamgulmlem5  24818  lgambdd  24822  lgamcvg2  24840  erdsze2lem1  24890  sinccvglem  25110  divcnvlin  25213  prodfclim1  25222  iprodefisum  25319  faclimlem2  25364  nodense  25645  nobnddown  25657  brbtwn2  25845  colinearalglem4  25849  supadd  26239  ltflcei  26240  lxflflp1  26242  opnmbllem0  26243  mblfinlem2  26245  mblfinlem3  26246  ismblfin  26248  itg2addnclem  26257  itg2addnclem2  26258  itg2addnclem3  26259  itg2addnc  26260  ibladdnclem  26262  ftc1cnnclem  26279  ftc1cnnc  26280  ftc1anc  26289  fnemeet1  26396  trirn  26458  geomcau  26466  prdsbnd  26503  cntotbnd  26506  heiborlem4  26524  rrndstprj2  26541  rrncmslem  26542  rrnequiv  26545  iccbnd  26550  lzenom  26829  icodiamlt  26884  irrapxlem2  26887  irrapxlem3  26888  irrapxlem5  26890  pellexlem2  26894  pell14qrgt0  26923  pellfundlb  26948  pellfundex  26950  pellfund14  26962  rmspecsqrnq  26970  jm2.24nn  27025  jm2.17a  27026  jm2.17b  27027  congabseq  27040  acongrep  27046  acongeq  27049  jm2.26lem3  27073  jm2.27a  27077  jm2.27c  27079  hbtlem2  27306  dgraaub  27331  f1otrspeq  27368  pmtrfrn  27378  pmtrfconj  27385  symggen  27389  psgnunilem4  27398  idomodle  27490  fmul01  27687  fmul01lt1lem1  27691  fmul01lt1lem2  27692  climrec  27706  climsuse  27711  stoweidlem1  27727  stoweidlem11  27737  stoweidlem13  27739  stoweidlem14  27740  stoweidlem16  27742  stoweidlem21  27747  stoweidlem25  27751  stoweidlem26  27752  stoweidlem36  27762  stoweidlem38  27764  stoweidlem41  27767  stoweidlem42  27768  stoweidlem45  27771  stoweidlem48  27774  stoweidlem52  27778  stoweidlem62  27788  wallispilem3  27793  stirlinglem5  27804  stirlinglem6  27805  stirlinglem7  27806  stirlinglem10  27809  stirlinglem12  27811  stirlinglem15  27814  ccatsymb  28180  2cshw2lem1  28253  2cshwid  28259  cshweqdif2  28271  cvlcvr1  30138  cvrat3  30240  dalem25  30496  cdlema1N  30589  dalawlem3  30671  dalawlem4  30672  dalawlem5  30673  dalawlem6  30674  dalawlem7  30675  dalawlem9  30677  dalawlem11  30679  dalawlem12  30680  lhp2lt  30799  lhpmcvr  30821  4atexlemcnd  30870  lautj  30891  trlle  30982  trlval3  30985  trlval4  30986  cdleme0moN  31023  cdleme13  31070  cdleme15  31076  cdleme19b  31102  cdleme20e  31111  cdleme20j  31116  cdleme22e  31142  cdleme22eALTN  31143  cdleme26fALTN  31160  cdleme26f  31161  cdleme27N  31167  cdleme41sn3a  31231  cdleme46fsvlpq  31303  cdlemeg46vrg  31325  cdlemg4  31415  cdlemg7N  31424  cdlemg9a  31430  cdlemg11b  31440  cdlemg12a  31441  trljco  31538  tendoidcl  31567  tendococl  31570  tendopltp  31578  tendo0tp  31587  tendoicl  31594  cdlemi2  31617  cdlemk5a  31633  cdlemk5  31634  cdlemk12  31648  cdlemkole  31651  cdlemk14  31652  cdlemk12u  31670  cdlemk37  31712  cdlemk39s-id  31738  cdlemk49  31749  cdlemk39u1  31765  cdlemk39u  31766  dian0  31838  cdlemm10N  31917  cdlemn2  31994  cdlemn10  32005  dihord1  32017  dihord10  32022  dihmeetlem4preN  32105  dihmeetlem18N  32123  dihmeetlem20N  32125  dihjatc  32216  mapdcnvatN  32465
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-rab 2715  df-v 2959  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-sn 3821  df-pr 3822  df-op 3824  df-br 4214
  Copyright terms: Public domain W3C validator