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

Theorem eqbrtrd 4707
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 4695 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbird 247 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523   class class class wbr 4685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686
This theorem is referenced by:  eqbrtrrd  4709  somin2  5566  en1b  8065  domunsncan  8101  fodomfi  8280  hartogslem1  8488  wemaplem2  8493  infdifsn  8592  carddomi2  8834  cdaun  9032  cda1dif  9036  mapcdaen  9044  cdaxpdom  9049  cdafi  9050  cdainf  9052  carden  9411  alephsuc3  9440  fpwwe2lem6  9495  fpwwe2lem7  9496  inar1  9635  rankcf  9637  lesub3d  10683  lbinfle  11016  supadd  11029  supmul  11033  rpnnen1lem3  11854  rpnnen1lem3OLD  11860  divge1  11936  xrmin1  12046  xrmin2  12047  ifle  12066  qbtwnxr  12069  xltnegi  12085  xleadd1a  12121  xlt2add  12128  xlemul1a  12156  xov1plusxeqvd  12356  ubmelm1fzo  12604  flflp1  12648  ceim1l  12686  ceilm1lt  12687  ceille  12689  quoremz  12694  quoremnn0ALT  12696  modlt  12719  modeqmodmin  12780  addmodlteq  12785  seqf1olem1  12880  bernneq  13030  discr  13041  faclbnd2  13118  faclbnd4lem3  13122  hashun2  13210  hashfun  13262  ccatsymb  13400  ccatrn  13407  sqrlem6  14032  sqrlem7  14033  rddif  14124  amgm2  14153  icodiamlt  14218  climconst  14318  rlimconst  14319  serclim0  14352  rlimcn1  14363  mulcn2  14370  reccn2  14371  o1mul  14389  o1rlimmul  14393  iserex  14431  climlec2  14433  iserge0  14435  climcau  14445  caucvgrlem  14447  caucvgr  14450  iseraltlem2  14457  iseraltlem3  14458  iseralt  14459  fsumabs  14577  o1fsum  14589  iserabs  14591  climfsum  14596  isumless  14621  climcndslem2  14626  divrcnv  14628  flo1  14630  supcvg  14632  georeclim  14647  geomulcvg  14651  cvgrat  14659  mertenslem1  14660  prodfclim1  14669  fprodge1  14770  fprodle  14771  efcvgfsum  14860  eftlub  14883  eflegeo  14895  tanhlt1  14934  tanhbnd  14935  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  cos01gt0  14965  ruclem2  15005  ruclem3  15006  ruclem9  15011  ruclem11  15013  ruclem12  15014  bitsfzolem  15203  bitsfzo  15204  bitsinv1lem  15210  sadcaddlem  15226  mulgcd  15312  eucalglt  15345  lcmledvds  15359  lcmfledvds  15392  mulgcddvds  15416  coprmproddvdslem  15423  prmind2  15445  isprm5  15466  divdenle  15504  nonsq  15514  pythagtriplem4  15571  pclem  15590  pcpremul  15595  pczdvds  15614  pcprmpw2  15633  qexpz  15652  prmreclem4  15670  prmreclem5  15671  4sqlem10  15698  ramtub  15763  ramub2  15765  prmodvdslcmf  15798  prmgaplem8  15809  natpropd  16683  catciso  16804  p0le  17090  acsdomd  17228  qusgrp  17696  f1otrspeq  17913  pmtrfrn  17924  pmtrfconj  17932  symggen  17936  psgnunilem4  17963  oddvds2  18029  odcau  18065  pgpfi  18066  pgpssslw  18075  sylow3lem4  18091  efgred2  18212  frgp0  18219  odadd2  18298  oddvdssubg  18304  ablfac1c  18516  ablfac1eu  18518  pgpfaclem3  18528  isabvd  18868  abvsubtri  18883  mplsubrg  19488  coe1sfi  19631  cyggic  19969  mp2pm2mplem5  20663  en2top  20837  1stcrest  21304  2ndcrest  21305  hausmapdom  21351  ufilen  21781  xmetrtri2  22208  prdsxmetlem  22220  bl2in  22252  xblcntrps  22262  xblcntr  22263  ssblps  22274  ssbl  22275  blssps  22276  blss  22277  blcld  22357  methaus  22372  metustexhalf  22408  nmtri2  22478  tngngp3  22507  nrginvrcnlem  22542  nrginvrcn  22543  nmoi  22579  nmo0  22586  nmoid  22593  blcvx  22648  reperflem  22668  reconnlem2  22677  metdcnlem  22686  metdscn  22706  metnrmlem3  22711  mulc1cncf  22755  iccpnfhmeo  22791  cnheiborlem  22800  cnheibor  22801  lebnumii  22812  pcopt  22868  pcopt2  22869  pcoass  22870  nmoleub2lem  22960  nmoleub2lem3  22961  nmoleub2lem2  22962  ipcau2  23079  tchcphlem1  23080  nglmle  23146  trirn  23229  rrxdstprj1  23238  minveclem3  23246  ivthlem2  23267  ivthlem3  23268  ivth2  23270  ovollb  23293  ovolsslem  23298  ovollb2lem  23302  ovolctb  23304  ovoliunlem1  23316  ovolsca  23329  ovolicc1  23330  ovolicc2lem4  23334  nulmbl  23349  ioombl1lem4  23375  uniioovol  23393  uniioombllem3a  23398  uniioombllem4  23400  opnmbllem  23415  volcn  23420  volivth  23421  i1fadd  23507  i1fmul  23508  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mbfi1fseqlem6  23532  itg2const2  23553  itg2seq  23554  itg2uba  23555  itg2split  23561  itg2monolem1  23562  itg2monolem3  23564  itg2i1fseq2  23568  itg2addlem  23570  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  itgless  23628  ibladdlem  23631  bddmulibl  23650  dveflem  23787  dvferm1lem  23792  dvferm2lem  23794  dvlip  23801  dvlipcn  23802  dvlip2  23803  dvle  23815  dvivthlem1  23816  lhop1lem  23821  dvcvx  23828  dvfsumabs  23831  dvfsumlem2  23835  dvfsumlem4  23837  dvfsumrlim2  23840  dvfsum2  23842  ftc1a  23845  ftc1lem4  23847  ftc1lem5  23848  deg1sub  23913  ply1divex  23941  deg1submon1p  23957  r1pdeglt  23963  dvdsq1p  23965  fta1glem2  23971  fta1g  23972  plyeq0lem  24011  dgrlt  24067  fta1lem  24107  aalioulem2  24133  aalioulem3  24134  aalioulem4  24135  aaliou3lem2  24143  aaliou3lem9  24150  taylply2  24167  ulmbdd  24197  ulmdvlem1  24199  mtest  24203  mtestbdd  24204  radcnvlem1  24212  radcnvle  24219  pserulm  24221  psercn  24225  pserdvlem2  24227  abelthlem2  24231  abelthlem5  24234  abelthlem7  24237  abelthlem8  24238  abelthlem9  24239  reeff1olem  24245  tangtx  24302  tanord  24329  efif1olem4  24336  logrnaddcl  24366  logcj  24397  logimul  24405  logneg2  24406  logdivlti  24411  divlogrlim  24426  logcnlem3  24435  logcnlem4  24436  efopn  24449  logtayllem  24450  logtayl  24451  cxpcn3lem  24533  cxpaddle  24538  abscxpbnd  24539  asinlem3  24643  asinneg  24658  asinsin  24664  atanlogaddlem  24685  atantan  24695  bndatandm  24701  atans2  24703  atantayl  24709  atantayl2  24710  atantayl3  24711  leibpi  24714  birthdaylem3  24725  rlimcnp  24737  efrlim  24741  cxplim  24743  cxp2lim  24748  cxploglim2  24750  divsqrtsumo1  24755  jensenlem2  24759  amgm  24762  logdifbnd  24765  harmonicbnd4  24782  fsumharmonic  24783  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamgulmlem5  24804  lgambdd  24808  lgamcvg2  24826  ftalem1  24844  ftalem5  24848  basellem1  24852  basellem8  24859  ppip1le  24932  ppiltx  24948  sqff1o  24953  chtublem  24981  chpub  24990  logfaclbnd  24992  logfacrlim  24994  logexprlim  24995  mersenne  24997  bcmono  25047  bcmax  25048  bposlem2  25055  bposlem5  25058  lgslem3  25069  gausslemma2dlem1a  25135  lgsquadlem1  25150  lgsquadlem2  25151  2lgslem1c  25163  2sqblem  25201  chebbnd1  25206  chtppilimlem1  25207  chto1ub  25210  chpchtlim  25213  chpo1ubb  25215  rplogsumlem1  25218  rplogsumlem2  25219  rpvmasumlem  25221  dchrisumlem1  25223  dchrisumlem2  25224  dchrmusum2  25228  dchrvmasumlem2  25232  dchrvmasumlem3  25233  dchrvmasumiflem1  25235  dchrisum0flblem1  25242  dchrisum0fno1  25245  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0lem2  25252  rplogsum  25261  mudivsum  25264  mulogsumlem  25265  mulog2sumlem1  25268  mulog2sumlem2  25269  vmalogdivsum2  25272  2vmadivsumlem  25274  selberglem2  25280  selberg2b  25286  logdivbnd  25290  selberg3lem1  25291  selberg3lem2  25292  selberg4lem1  25294  pntrmax  25298  pntrsumo1  25299  pntrlog2bndlem1  25311  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntrlog2bnd  25318  pntpbnd1a  25319  pntpbnd2  25321  pntibndlem2  25325  pntlemb  25331  pntlemg  25332  pntlemh  25333  pntlemr  25336  pntlemj  25337  pntlemf  25339  pntlemo  25341  pnt  25348  padicabv  25364  ostth2lem2  25368  ostth2lem3  25369  ostth3  25372  colperpexlem3  25669  mideulem2  25671  lnperpex  25740  trgcopy  25741  iscgra1  25747  brbtwn2  25830  colinearalglem4  25834  subupgr  26224  crctcshwlkn0lem1  26758  nvabs  27655  nvge0  27656  smcnlem  27680  nmblolbii  27782  blocnilem  27787  siii  27836  ubthlem2  27855  minvecolem3  27860  htthlem  27902  bcsiALT  28164  bcs3  28168  chscllem4  28627  0cnop  28966  0cnfn  28967  nmbdoplbi  29011  nmcoplbi  29015  nmophmi  29018  nmbdfnlbi  29036  nmcfnlbi  29039  nlelchi  29048  riesz1  29052  cnlnadjlem2  29055  nmopadjlei  29075  nmoptrii  29081  nmopcoi  29082  nmopcoadji  29088  unierri  29091  branmfn  29092  pjs14i  29197  hstle  29217  cdj3lem2b  29424  xlt2addrd  29651  eliccelico  29667  elicoelioo  29668  ltesubnnd  29696  archirngz  29871  archiabllem2c  29877  madjusmdetlem2  30022  locfinref  30036  sqsscirc1  30082  tpr2rico  30086  esumcst  30253  esumgect  30280  esum2d  30283  measunl  30407  measiun  30409  omssubaddlem  30489  omssubadd  30490  carsgsigalem  30505  carsgclctunlem2  30509  pmeasmono  30514  eulerpartlemgc  30552  eulerpartlemb  30558  ballotlemsel1i  30702  ballotlemro  30712  sgnsub  30734  signsplypnf  30755  signsply0  30756  signsvtn  30789  signsvfnn  30791  hgt750lemd  30854  logdivsqrle  30856  erdsze2lem1  31311  sinccvglem  31692  divcnvlin  31744  iprodefisum  31753  faclimlem2  31756  nosep1o  31957  nodense  31967  fnemeet1  32486  dnibndlem10  32602  dnibndlem11  32603  dnibnd  32606  knoppcnlem4  32611  knoppcnlem6  32613  unblimceq0lem  32622  unblimceq0  32623  unbdqndv2lem1  32625  unbdqndv2lem2  32626  knoppndvlem11  32638  knoppndvlem12  32639  knoppndvlem14  32641  knoppndvlem15  32642  knoppndvlem17  32644  knoppndvlem18  32645  knoppndvlem19  32646  knoppndvlem21  32648  ltflcei  33527  ptrecube  33539  poimirlem16  33555  poimirlem17  33556  poimirlem29  33568  broucube  33573  opnmbllem0  33575  mblfinlem2  33577  mblfinlem3  33578  ismblfin  33580  itg2addnclem  33591  itg2addnclem2  33592  itg2addnclem3  33593  itg2addnc  33594  ibladdnclem  33596  ftc1cnnclem  33613  ftc1cnnc  33614  ftc1anc  33623  geomcau  33685  prdsbnd  33722  cntotbnd  33725  heiborlem4  33743  rrndstprj2  33760  rrncmslem  33761  rrnequiv  33764  iccbnd  33769  cvlcvr1  34944  cvrat3  35046  dalem25  35302  cdlema1N  35395  dalawlem3  35477  dalawlem4  35478  dalawlem5  35479  dalawlem6  35480  dalawlem7  35481  dalawlem9  35483  dalawlem11  35485  dalawlem12  35486  lhp2lt  35605  lhpmcvr  35627  4atexlemcnd  35676  lautj  35697  trlle  35789  trlval3  35792  trlval4  35793  cdleme0moN  35830  cdleme13  35877  cdleme15  35883  cdleme19b  35909  cdleme20e  35918  cdleme20j  35923  cdleme22e  35949  cdleme22eALTN  35950  cdleme26fALTN  35967  cdleme26f  35968  cdleme27N  35974  cdleme41sn3a  36038  cdleme46fsvlpq  36110  cdlemeg46vrg  36132  cdlemg4  36222  cdlemg7N  36231  cdlemg9a  36237  cdlemg11b  36247  cdlemg12a  36248  trljco  36345  tendoidcl  36374  tendococl  36377  tendopltp  36385  tendo0tp  36394  tendoicl  36401  cdlemi2  36424  cdlemk5a  36440  cdlemk5  36441  cdlemk12  36455  cdlemkole  36458  cdlemk14  36459  cdlemk12u  36477  cdlemk37  36519  cdlemk39s-id  36545  cdlemk49  36556  cdlemk39u1  36572  cdlemk39u  36573  dian0  36645  cdlemm10N  36724  cdlemn2  36801  cdlemn10  36812  dihord1  36824  dihord10  36829  dihmeetlem4preN  36912  dihmeetlem18N  36930  dihmeetlem20N  36932  dihjatc  37023  mapdcnvatN  37272  lzenom  37650  irrapxlem2  37704  irrapxlem3  37705  irrapxlem5  37707  pellexlem2  37711  pell14qrgt0  37740  pellfundlb  37765  pellfundex  37767  pellfund14  37779  rmspecsqrtnq  37787  rmspecsqrtnqOLD  37788  jm2.24nn  37843  jm2.17a  37844  jm2.17b  37845  congabseq  37858  acongrep  37864  acongeq  37867  jm2.26lem3  37885  jm2.27a  37889  jm2.27c  37891  hbtlem2  38011  dgraaub  38035  idomodle  38091  relexpxpmin  38326  frege102d  38363  hashnzfzclim  38838  binomcxplemfrat  38867  binomcxplemnotnn0  38872  suprnmpt  39669  mpct  39707  rnmptbddlem  39769  dstregt0  39807  lefldiveq  39819  fzisoeu  39828  upbdrech  39833  ssfiunibd  39837  fzdifsuc2  39838  xadd0ge  39849  supxrgere  39862  supxrge  39867  suplesup  39868  xrlexaddrp  39881  infxrunb2  39897  infleinflem2  39900  reclt0d  39920  infrpgernmpt  40008  ioondisj2  40032  iccshift  40062  iooshift  40066  fmul01  40130  fmul01lt1lem1  40134  fmul01lt1lem2  40135  climrec  40153  climsuse  40158  mullimc  40166  mullimcf  40173  constlimc  40174  idlimc  40176  divcnvg  40177  limcperiod  40178  limcrecl  40179  lptioo2  40181  lptioo1  40182  islpcn  40189  lptre2pt  40190  limcleqr  40194  neglimc  40197  addlimc  40198  0ellimcdiv  40199  limclner  40201  climleltrp  40226  limsuplesup  40249  limsupmnflem  40270  supcnvlimsupmpt  40291  0cnv  40292  xlimconst  40369  sinaover2ne0  40397  cncfshift  40405  cncfperiod  40410  cncfioobdlem  40427  cncfioobd  40428  fperdvper  40451  dvdivbd  40456  dvbdfbdioolem1  40461  dvbdfbdioolem2  40462  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnmul  40476  dvnprodlem1  40479  itgiccshift  40514  itgperiod  40515  ismbl3  40521  ovolsplit  40523  stoweidlem1  40536  stoweidlem11  40546  stoweidlem13  40548  stoweidlem14  40549  stoweidlem16  40551  stoweidlem21  40556  stoweidlem25  40560  stoweidlem26  40561  stoweidlem36  40571  stoweidlem38  40573  stoweidlem41  40576  stoweidlem42  40577  stoweidlem45  40580  stoweidlem48  40583  stoweidlem52  40587  stoweidlem62  40597  wallispilem3  40602  stirlinglem5  40613  stirlinglem6  40614  stirlinglem7  40615  stirlinglem10  40618  stirlinglem12  40620  stirlinglem15  40623  dirkercncflem1  40638  fourierdlem10  40652  fourierdlem12  40654  fourierdlem15  40657  fourierdlem16  40658  fourierdlem19  40661  fourierdlem20  40662  fourierdlem21  40663  fourierdlem22  40664  fourierdlem24  40666  fourierdlem30  40672  fourierdlem37  40679  fourierdlem39  40681  fourierdlem40  40682  fourierdlem41  40683  fourierdlem42  40684  fourierdlem47  40688  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem52  40693  fourierdlem54  40695  fourierdlem60  40701  fourierdlem61  40702  fourierdlem63  40704  fourierdlem64  40705  fourierdlem68  40709  fourierdlem71  40712  fourierdlem72  40713  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem77  40718  fourierdlem78  40719  fourierdlem79  40720  fourierdlem81  40722  fourierdlem82  40723  fourierdlem83  40724  fourierdlem84  40725  fourierdlem87  40728  fourierdlem92  40733  fourierdlem93  40734  fourierdlem94  40735  fourierdlem101  40742  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  fourierdlem114  40755  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  elaa2lem  40768  etransclem23  40792  etransclem28  40797  etransclem32  40801  etransclem35  40804  etransclem48  40817  qndenserrnbllem  40832  rrnprjdstle  40839  ioorrnopnlem  40842  ioorrnopnxrlem  40844  salexct  40870  sge0fsum  40922  sge0supre  40924  sge0rnbnd  40928  sge0lefi  40933  sge0lessmpt  40934  sge0ltfirp  40935  sge0prle  40936  sge0resrnlem  40938  sge0le  40942  sge0split  40944  sge0iunmptlemre  40950  sge0iunmpt  40953  sge0isum  40962  sge0xaddlem1  40968  sge0xaddlem2  40969  sge0xadd  40970  sge0reuz  40982  sge0reuzb  40983  meaunle  40999  meaiunlelem  41003  voliunsge0lem  41007  meaiuninc  41016  meaiininclem  41021  omeunle  41051  omeiunle  41052  omelesplit  41053  omeiunltfirp  41054  carageniuncllem2  41057  caratheodorylem2  41062  caragencmpl  41070  ovnlecvr  41093  ovncvrrp  41099  ovnsubaddlem1  41105  ovnsubadd  41107  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem5  41134  hoidmvle  41135  ovnhoilem1  41136  ovnlecvr2  41145  ovncvr2  41146  hoiqssbllem2  41158  hspmbllem2  41162  hspmbllem3  41163  ovnsplit  41183  ovolval5lem1  41187  vonioolem1  41215  vonioolem2  41216  vonicclem1  41218  vonicclem2  41219  pimconstlt1  41236  smflimlem2  41301  smflimlem4  41303  smfmullem1  41319  smfsuplem1  41338  smflimsuplem4  41350  smflimsuplem5  41351  iccpartltu  41686  iccpartleu  41689  pgrple2abl  42471  difmodm1lt  42642  nnpw2blen  42699  dignn0flhalflem1  42734
  Copyright terms: Public domain W3C validator