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

Theorem eqbrtrd 5080
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
Hypotheses
Ref Expression
eqbrtrd.1 (𝜑𝐴 = 𝐵)
eqbrtrd.2 (𝜑𝐵𝑅𝐶)
Assertion
Ref Expression
eqbrtrd (𝜑𝐴𝑅𝐶)

Proof of Theorem eqbrtrd
StepHypRef Expression
1 eqbrtrd.2 . 2 (𝜑𝐵𝑅𝐶)
2 eqbrtrd.1 . . 3 (𝜑𝐴 = 𝐵)
32breq1d 5068 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbird 258 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528   class class class wbr 5058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059
This theorem is referenced by:  eqbrtrrd  5082  somin2  5989  en1b  8566  domunsncan  8606  fodomfi  8786  infsupprpr  8957  hartogslem1  8995  wemaplem2  9000  infdifsn  9109  carddomi2  9388  djuinf  9603  carden  9962  alephsuc3  9991  fpwwe2lem6  10046  fpwwe2lem7  10047  inar1  10186  rankcf  10188  lesub3d  11247  lbinfle  11585  supadd  11598  supmul  11602  rpnnen1lem3  12368  divge1  12447  xrmin1  12560  xrmin2  12561  ifle  12580  qbtwnxr  12583  xltnegi  12599  xleadd1a  12636  xlt2add  12643  xlemul1a  12671  xov1plusxeqvd  12874  ubmelm1fzo  13123  flflp1  13167  ceim1l  13205  ceilm1lt  13206  ceille  13208  quoremz  13213  quoremnn0ALT  13215  modlt  13238  modeqmodmin  13299  addmodlteq  13304  seqf1olem1  13399  bernneq  13580  discr  13591  faclbnd2  13641  faclbnd4lem3  13645  hashun2  13734  hashfun  13788  ccatsymb  13926  ccatrn  13933  sqrlem6  14597  sqrlem7  14598  rddif  14690  amgm2  14719  icodiamlt  14785  climconst  14890  rlimconst  14891  serclim0  14924  rlimcn1  14935  mulcn2  14942  reccn2  14943  o1mul  14961  o1rlimmul  14965  iserex  15003  climlec2  15005  iserge0  15007  climcau  15017  caucvgrlem  15019  caucvgr  15022  iseraltlem2  15029  iseraltlem3  15030  iseralt  15031  fsumabs  15146  o1fsum  15158  iserabs  15160  climfsum  15165  isumless  15190  climcndslem2  15195  divrcnv  15197  flo1  15199  supcvg  15201  georeclim  15218  geomulcvg  15222  cvgrat  15229  mertenslem1  15230  prodfclim1  15239  fprodle  15340  efcvgfsum  15429  eftlub  15452  eflegeo  15464  tanhlt1  15503  tanhbnd  15504  ef01bndlem  15527  sin01bnd  15528  cos01bnd  15529  cos01gt0  15534  ruclem2  15575  ruclem3  15576  ruclem9  15581  ruclem11  15583  ruclem12  15584  bitsfzolem  15773  bitsfzo  15774  bitsinv1lem  15780  sadcaddlem  15796  mulgcd  15886  eucalglt  15919  lcmledvds  15933  lcmfledvds  15966  mulgcddvds  15989  coprmproddvdslem  15996  prmind2  16019  isprm5  16041  divdenle  16079  nonsq  16089  pythagtriplem4  16146  pclem  16165  pcpremul  16170  pczdvds  16189  pcprmpw2  16208  qexpz  16227  prmreclem4  16245  prmreclem5  16246  4sqlem10  16273  ramtub  16338  ramub2  16340  prmodvdslcmf  16373  prmgaplem8  16384  natpropd  17236  catciso  17357  p0le  17643  acsdomd  17781  triv1nsgd  18265  qusgrp  18275  f1otrspeq  18506  pmtrfrn  18517  pmtrfconj  18525  symggen  18529  psgnunilem4  18556  oddvds2  18624  odcau  18660  pgpfi  18661  pgpssslw  18670  sylow3lem4  18686  efgred2  18810  frgp0  18817  odadd2  18900  oddvdssubg  18906  ablfac1c  19124  ablfac1eu  19126  pgpfaclem3  19136  2nsgsimpgd  19155  isabvd  19522  abvsubtri  19537  mplsubrg  20150  coe1sfi  20311  cyggic  20649  mp2pm2mplem5  21348  en2top  21523  1stcrest  21991  2ndcrest  21992  hausmapdom  22038  ufilen  22468  xmetrtri2  22895  prdsxmetlem  22907  bl2in  22939  xblcntrps  22949  xblcntr  22950  ssblps  22961  ssbl  22962  blssps  22963  blss  22964  blcld  23044  methaus  23059  metustexhalf  23095  nmtri2  23165  tngngp3  23194  nrginvrcnlem  23229  nrginvrcn  23230  nmoi  23266  nmo0  23273  nmoid  23280  blcvx  23335  reperflem  23355  reconnlem2  23364  metdcnlem  23373  metdscn  23393  metnrmlem3  23398  mulc1cncf  23442  iccpnfhmeo  23478  cnheiborlem  23487  cnheibor  23488  lebnumii  23499  pcopt  23555  pcopt2  23556  pcoass  23557  nmoleub2lem  23647  nmoleub2lem3  23648  nmoleub2lem2  23649  ipcau2  23766  tcphcphlem1  23767  nglmle  23834  trirn  23932  rrxdstprj1  23941  minveclem3  23961  ivthlem2  23982  ivthlem3  23983  ivth2  23985  ovollb  24009  ovolsslem  24014  ovollb2lem  24018  ovolctb  24020  ovoliunlem1  24032  ovolsca  24045  ovolicc1  24046  ovolicc2lem4  24050  nulmbl  24065  ioombl1lem4  24091  uniioovol  24109  uniioombllem3a  24114  uniioombllem4  24116  opnmbllem  24131  volcn  24136  volivth  24137  i1fadd  24225  i1fmul  24226  mbfi1fseqlem4  24248  mbfi1fseqlem5  24249  mbfi1fseqlem6  24250  itg2const2  24271  itg2seq  24272  itg2uba  24273  itg2split  24279  itg2monolem1  24280  itg2monolem3  24282  itg2i1fseq2  24286  itg2addlem  24288  itg2gt0  24290  itg2cnlem1  24291  itg2cnlem2  24292  itgless  24346  ibladdlem  24349  bddmulibl  24368  dveflem  24505  dvferm1lem  24510  dvferm2lem  24512  dvlip  24519  dvlipcn  24520  dvlip2  24521  dvle  24533  dvivthlem1  24534  lhop1lem  24539  dvcvx  24546  dvfsumabs  24549  dvfsumlem2  24553  dvfsumlem4  24555  dvfsumrlim2  24558  dvfsum2  24560  ftc1a  24563  ftc1lem4  24565  ftc1lem5  24566  deg1sub  24631  ply1divex  24659  deg1submon1p  24675  r1pdeglt  24681  dvdsq1p  24683  fta1glem2  24689  fta1g  24690  plyeq0lem  24729  dgrlt  24785  fta1lem  24825  aalioulem2  24851  aalioulem3  24852  aalioulem4  24853  aaliou3lem2  24861  aaliou3lem9  24868  taylply2  24885  ulmbdd  24915  ulmdvlem1  24917  mtest  24921  mtestbdd  24922  radcnvlem1  24930  radcnvle  24937  pserulm  24939  psercn  24943  pserdvlem2  24945  abelthlem2  24949  abelthlem5  24952  abelthlem7  24955  abelthlem8  24956  abelthlem9  24957  reeff1olem  24963  tangtx  25020  tanord  25049  efif1olem4  25056  logrnaddcl  25085  logcj  25116  logimul  25124  logneg2  25125  logdivlti  25130  divlogrlim  25145  logcnlem3  25154  logcnlem4  25155  efopn  25168  logtayllem  25169  logtayl  25170  cxpcn3lem  25255  cxpaddle  25260  abscxpbnd  25261  asinlem3  25376  asinneg  25391  asinsin  25397  atanlogaddlem  25418  atantan  25428  bndatandm  25434  atans2  25436  atantayl  25442  atantayl2  25443  atantayl3  25444  leibpi  25448  birthdaylem3  25459  rlimcnp  25471  efrlim  25475  cxplim  25477  cxp2lim  25482  cxploglim2  25484  divsqrtsumo1  25489  jensenlem2  25493  amgm  25496  logdifbnd  25499  harmonicbnd4  25516  fsumharmonic  25517  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamgulmlem5  25538  lgambdd  25542  lgamcvg2  25560  ftalem1  25578  ftalem5  25582  basellem1  25586  basellem8  25593  ppip1le  25666  ppiltx  25682  sqff1o  25687  chtublem  25715  chpub  25724  logfaclbnd  25726  logfacrlim  25728  logexprlim  25729  mersenne  25731  bcmono  25781  bcmax  25782  bposlem2  25789  bposlem5  25792  lgslem3  25803  gausslemma2dlem1a  25869  lgsquadlem1  25884  lgsquadlem2  25885  2lgslem1c  25897  2sqblem  25935  chebbnd1  25976  chtppilimlem1  25977  chto1ub  25980  chpchtlim  25983  chpo1ubb  25985  rplogsumlem1  25988  rplogsumlem2  25989  rpvmasumlem  25991  dchrisumlem1  25993  dchrisumlem2  25994  dchrmusum2  25998  dchrvmasumlem2  26002  dchrvmasumlem3  26003  dchrvmasumiflem1  26005  dchrisum0flblem1  26012  dchrisum0fno1  26015  dchrisum0lem1b  26019  dchrisum0lem1  26020  dchrisum0lem2a  26021  dchrisum0lem2  26022  rplogsum  26031  mudivsum  26034  mulogsumlem  26035  mulog2sumlem1  26038  mulog2sumlem2  26039  vmalogdivsum2  26042  2vmadivsumlem  26044  selberglem2  26050  selberg2b  26056  logdivbnd  26060  selberg3lem1  26061  selberg3lem2  26062  selberg4lem1  26064  pntrmax  26068  pntrsumo1  26069  pntrlog2bndlem1  26081  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bnd  26088  pntpbnd1a  26089  pntpbnd2  26091  pntibndlem2  26095  pntlemb  26101  pntlemg  26102  pntlemh  26103  pntlemr  26106  pntlemj  26107  pntlemf  26109  pntlemo  26111  pnt  26118  padicabv  26134  ostth2lem2  26138  ostth2lem3  26139  ostth3  26142  colperpexlem3  26446  mideulem2  26448  lnperpex  26517  trgcopy  26518  iscgra1  26524  brbtwn2  26619  colinearalglem4  26623  subupgr  26997  crctcshwlkn0lem1  27516  nvabs  28377  nvge0  28378  smcnlem  28402  nmblolbii  28504  blocnilem  28509  siii  28558  ubthlem2  28576  minvecolem3  28581  htthlem  28622  bcsiALT  28884  bcs3  28888  chscllem4  29345  0cnop  29684  0cnfn  29685  nmbdoplbi  29729  nmcoplbi  29733  nmophmi  29736  nmbdfnlbi  29754  nmcfnlbi  29757  nlelchi  29766  riesz1  29770  cnlnadjlem2  29773  nmopadjlei  29793  nmoptrii  29799  nmopcoi  29800  nmopcoadji  29806  unierri  29809  branmfn  29810  pjs14i  29915  hstle  29935  cdj3lem2b  30142  xlt2addrd  30409  eliccelico  30427  elicoelioo  30428  ltesubnnd  30466  wrdt2ind  30555  archirngz  30746  archiabllem2c  30752  madjusmdetlem2  30993  locfinref  31005  sqsscirc1  31051  tpr2rico  31055  esumcst  31222  esumgect  31249  esum2d  31252  measunl  31375  measiun  31377  omssubaddlem  31457  omssubadd  31458  carsgsigalem  31473  carsgclctunlem2  31477  pmeasmono  31482  eulerpartlemgc  31520  eulerpartlemb  31526  ballotlemsel1i  31670  ballotlemro  31680  sgnsub  31702  signsplypnf  31720  signsply0  31721  signsvtn  31754  signsvfnn  31756  hgt750lemd  31819  logdivsqrle  31821  hashf1dmcdm  32254  erdsze2lem1  32348  sinccvglem  32813  divcnvlin  32862  iprodefisum  32871  faclimlem2  32874  nosep1o  33084  nodense  33094  fnemeet1  33612  dnibndlem10  33724  dnibndlem11  33725  dnibnd  33728  knoppcnlem4  33733  knoppcnlem6  33735  unblimceq0lem  33743  unbdqndv2lem1  33746  unbdqndv2lem2  33747  knoppndvlem11  33759  knoppndvlem12  33760  knoppndvlem14  33762  knoppndvlem15  33763  knoppndvlem17  33765  knoppndvlem18  33766  knoppndvlem19  33767  knoppndvlem21  33769  ctbssinf  34570  ltflcei  34762  ptrecube  34774  poimirlem16  34790  poimirlem17  34791  poimirlem29  34803  broucube  34808  opnmbllem0  34810  mblfinlem2  34812  mblfinlem3  34813  ismblfin  34815  itg2addnclem  34825  itg2addnclem2  34826  itg2addnclem3  34827  itg2addnc  34828  ibladdnclem  34830  ftc1cnnclem  34847  ftc1cnnc  34848  ftc1anc  34857  geomcau  34917  prdsbnd  34954  cntotbnd  34957  heiborlem4  34975  rrndstprj2  34992  rrncmslem  34993  rrnequiv  34996  iccbnd  35001  cvlcvr1  36357  cvrat3  36460  dalem25  36716  cdlema1N  36809  dalawlem3  36891  dalawlem4  36892  dalawlem5  36893  dalawlem6  36894  dalawlem7  36895  dalawlem9  36897  dalawlem11  36899  dalawlem12  36900  lhp2lt  37019  lhpmcvr  37041  4atexlemcnd  37090  lautj  37111  trlle  37202  trlval3  37205  trlval4  37206  cdleme0moN  37243  cdleme13  37290  cdleme15  37296  cdleme19b  37322  cdleme20e  37331  cdleme20j  37336  cdleme22e  37362  cdleme22eALTN  37363  cdleme26fALTN  37380  cdleme26f  37381  cdleme27N  37387  cdleme41sn3a  37451  cdleme46fsvlpq  37523  cdlemeg46vrg  37545  cdlemg4  37635  cdlemg7N  37644  cdlemg9a  37650  cdlemg11b  37660  cdlemg12a  37661  trljco  37758  tendoidcl  37787  tendococl  37790  tendopltp  37798  tendo0tp  37807  tendoicl  37814  cdlemi2  37837  cdlemk5a  37853  cdlemk5  37854  cdlemk12  37868  cdlemkole  37871  cdlemk14  37872  cdlemk12u  37890  cdlemk37  37932  cdlemk39s-id  37958  cdlemk49  37969  cdlemk39u1  37985  cdlemk39u  37986  dian0  38057  cdlemm10N  38136  cdlemn2  38213  cdlemn10  38224  dihord1  38236  dihord10  38241  dihmeetlem4preN  38324  dihmeetlem18N  38342  dihmeetlem20N  38344  dihjatc  38435  mapdcnvatN  38684  fltltc  39153  lzenom  39247  irrapxlem2  39300  irrapxlem3  39301  irrapxlem5  39303  pellexlem2  39307  pell14qrgt0  39336  pellfundlb  39361  pellfundex  39363  pellfund14  39375  rmspecsqrtnq  39383  jm2.24nn  39436  jm2.17a  39437  jm2.17b  39438  congabseq  39451  acongrep  39457  acongeq  39460  jm2.26lem3  39478  jm2.27a  39482  jm2.27c  39484  hbtlem2  39604  dgraaub  39628  idomodle  39676  relexpxpmin  39942  frege102d  39979  hashnzfzclim  40534  binomcxplemfrat  40563  binomcxplemnotnn0  40568  suprnmpt  41310  mpct  41344  rnmptbddlem  41395  dstregt0  41427  lefldiveq  41439  fzisoeu  41447  upbdrech  41452  ssfiunibd  41456  fzdifsuc2  41457  xadd0ge  41468  supxrgere  41481  supxrge  41486  suplesup  41487  xrlexaddrp  41500  infxrunb2  41516  infleinflem2  41519  reclt0d  41538  infrpgernmpt  41621  ioondisj2  41647  iccshift  41674  iooshift  41678  fmul01  41741  fmul01lt1lem1  41745  fmul01lt1lem2  41746  climrec  41764  climsuse  41769  mullimc  41777  mullimcf  41784  constlimc  41785  idlimc  41787  divcnvg  41788  limcperiod  41789  limcrecl  41790  lptioo2  41792  lptioo1  41793  islpcn  41800  lptre2pt  41801  limcleqr  41805  neglimc  41808  addlimc  41809  0ellimcdiv  41810  limclner  41812  climleltrp  41837  limsuplesup  41860  limsupmnflem  41881  supcnvlimsupmpt  41902  0cnv  41903  xlimconst  41986  xlimliminflimsup  42023  sinaover2ne0  42029  cncfshift  42037  cncfperiod  42042  cncfioobdlem  42059  cncfioobd  42060  fperdvper  42083  dvdivbd  42088  dvbdfbdioolem1  42093  dvbdfbdioolem2  42094  ioodvbdlimc1lem1  42096  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnmul  42108  dvnprodlem1  42111  itgiccshift  42145  itgperiod  42146  ismbl3  42152  ovolsplit  42154  stoweidlem1  42167  stoweidlem11  42177  stoweidlem13  42179  stoweidlem14  42180  stoweidlem16  42182  stoweidlem21  42187  stoweidlem25  42191  stoweidlem26  42192  stoweidlem36  42202  stoweidlem38  42204  stoweidlem41  42207  stoweidlem42  42208  stoweidlem45  42211  stoweidlem48  42214  stoweidlem52  42218  stoweidlem62  42228  wallispilem3  42233  stirlinglem5  42244  stirlinglem6  42245  stirlinglem7  42246  stirlinglem10  42249  stirlinglem12  42251  stirlinglem15  42254  dirkercncflem1  42269  fourierdlem10  42283  fourierdlem12  42285  fourierdlem15  42288  fourierdlem16  42289  fourierdlem19  42292  fourierdlem20  42293  fourierdlem21  42294  fourierdlem22  42295  fourierdlem24  42297  fourierdlem30  42303  fourierdlem37  42310  fourierdlem39  42312  fourierdlem40  42313  fourierdlem41  42314  fourierdlem42  42315  fourierdlem47  42319  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem52  42324  fourierdlem54  42326  fourierdlem60  42332  fourierdlem61  42333  fourierdlem63  42335  fourierdlem64  42336  fourierdlem68  42340  fourierdlem71  42343  fourierdlem72  42344  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem76  42348  fourierdlem77  42349  fourierdlem78  42350  fourierdlem79  42351  fourierdlem81  42353  fourierdlem82  42354  fourierdlem83  42355  fourierdlem84  42356  fourierdlem87  42359  fourierdlem92  42364  fourierdlem93  42365  fourierdlem94  42366  fourierdlem101  42373  fourierdlem102  42374  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  fourierdlem112  42384  fourierdlem113  42385  fourierdlem114  42386  sqwvfoura  42394  sqwvfourb  42395  fouriersw  42397  elaa2lem  42399  etransclem23  42423  etransclem28  42428  etransclem32  42432  etransclem35  42435  etransclem48  42448  qndenserrnbllem  42460  rrnprjdstle  42467  ioorrnopnlem  42470  ioorrnopnxrlem  42472  salexct  42498  sge0fsum  42550  sge0supre  42552  sge0rnbnd  42556  sge0lefi  42561  sge0lessmpt  42562  sge0ltfirp  42563  sge0prle  42564  sge0resrnlem  42566  sge0le  42570  sge0split  42572  sge0iunmptlemre  42578  sge0iunmpt  42581  sge0isum  42590  sge0xaddlem1  42596  sge0xaddlem2  42597  sge0xadd  42598  sge0reuz  42610  sge0reuzb  42611  meaunle  42627  meaiunlelem  42631  voliunsge0lem  42635  meaiuninc  42644  meaiininclem  42649  omeunle  42679  omeiunle  42680  omelesplit  42681  omeiunltfirp  42682  carageniuncllem2  42685  caratheodorylem2  42690  caragencmpl  42698  ovnlecvr  42721  ovncvrrp  42727  ovnsubaddlem1  42733  ovnsubadd  42735  hoidmv1lelem1  42754  hoidmv1lelem2  42755  hoidmv1le  42757  hoidmvlelem1  42758  hoidmvlelem2  42759  hoidmvlelem5  42762  hoidmvle  42763  ovnhoilem1  42764  ovnlecvr2  42773  ovncvr2  42774  hoiqssbllem2  42786  hspmbllem2  42790  hspmbllem3  42791  ovnsplit  42811  ovolval5lem1  42815  vonioolem1  42843  vonioolem2  42844  vonicclem1  42846  vonicclem2  42847  pimconstlt1  42864  smflimlem2  42929  smflimlem4  42931  smfmullem1  42947  smfsuplem1  42966  smflimsuplem4  42978  smflimsuplem5  42979  iccpartltu  43432  iccpartleu  43435  pgrple2abl  44311  difmodm1lt  44480  nnpw2blen  44538  dignn0flhalflem1  44573  2itscp  44666
  Copyright terms: Public domain W3C validator