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

Theorem 3brtr4d 4717
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
Hypotheses
Ref Expression
3brtr4d.1 (𝜑𝐴𝑅𝐵)
3brtr4d.2 (𝜑𝐶 = 𝐴)
3brtr4d.3 (𝜑𝐷 = 𝐵)
Assertion
Ref Expression
3brtr4d (𝜑𝐶𝑅𝐷)

Proof of Theorem 3brtr4d
StepHypRef Expression
1 3brtr4d.1 . 2 (𝜑𝐴𝑅𝐵)
2 3brtr4d.2 . . 3 (𝜑𝐶 = 𝐴)
3 3brtr4d.3 . . 3 (𝜑𝐷 = 𝐵)
42, 3breq12d 4698 . 2 (𝜑 → (𝐶𝑅𝐷𝐴𝑅𝐵))
51, 4mpbird 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:  f1oiso2  6642  sucdom2  8197  ordtypelem6  8469  cdaen  9033  cdacomen  9041  cdadom1  9046  fin23lem26  9185  distrnq  9821  lediv12a  10954  recp1lt1  10959  ifle  12066  xleadd1a  12121  xlemul1a  12156  fldiv4p1lem1div2  12676  fldiv4lem1div2  12678  quoremz  12694  quoremnn0ALT  12696  intfracq  12698  modmulnn  12728  fzennn  12807  monoord2  12872  expgt1  12938  leexp2r  12958  leexp1a  12959  bernneq  13030  expmulnbnd  13036  digit1  13038  faclbnd  13117  faclbnd4lem3  13122  faclbnd4lem4  13123  faclbnd6  13126  facubnd  13127  hashdomi  13207  fzsdom2  13253  absrele  14092  absimle  14093  abstri  14114  abs2difabs  14118  limsupval2  14255  rlimrege0  14354  rlimrecl  14355  climsqz  14415  climsqz2  14416  rlimdiv  14420  rlimsqz  14424  rlimsqz2  14425  isercolllem1  14439  isercoll2  14443  fsumcvg2  14502  fsumrlim  14587  o1fsum  14589  cvgcmpce  14594  isumle  14620  climcndslem1  14625  climcndslem2  14626  harmonic  14635  expcnv  14640  explecnv  14641  geomulcvg  14651  efcllem  14852  ege2le3  14864  eflegeo  14895  rpnnen2lem4  14990  ruclem2  15005  ruclem8  15010  fsumdvds  15077  phibnd  15523  iserodd  15587  pcdvdstr  15627  pcprmpw2  15633  pockthg  15657  prmreclem4  15670  prmolefac  15797  2expltfac  15846  mod2ile  17153  odsubdvds  18032  pgpfi  18066  fislw  18086  efgredlemd  18203  efgredlem  18206  frgpcpbl  18218  abvres  18887  abvtrivd  18888  znrrg  19962  cstucnd  22135  psmetge0  22164  psmetres2  22166  xmetge0  22196  xmetres2  22213  imasf1oxmet  22227  comet  22365  stdbdxmet  22367  dscmet  22424  nrmmetd  22426  nmrtri  22475  tngngp  22505  nmolb2d  22569  nmoleub  22582  nmoco  22588  nmotri  22590  nmoid  22593  nmods  22595  cnmet  22622  xrsxmet  22659  metdstri  22701  metnrmlem3  22711  lebnumlem3  22809  ipcau2  23079  tchcphlem1  23080  tchcph  23082  trirn  23229  rrxmet  23237  rrxdstprj1  23238  minveclem2  23243  ovolunlem1a  23310  ovolscalem1  23327  volss  23347  voliunlem1  23364  volcn  23420  itg1climres  23526  mbfi1fseqlem5  23531  mbfi1fseqlem6  23532  itg2const2  23553  itg2seq  23554  itg2mulc  23559  itg2splitlem  23560  itg2monolem1  23562  itg2i1fseqle  23566  itg2i1fseq  23567  itg2i1fseq2  23568  itg2addlem  23570  itg2cnlem1  23573  itg2cnlem2  23574  iblss  23616  itgle  23621  ibladdlem  23631  iblabs  23640  iblabsr  23641  iblmulc2  23642  itgabs  23646  bddmulibl  23650  dvfsumabs  23831  dvfsumlem2  23835  dvfsum2  23842  deg1suble  23912  deg1mul3le  23921  plyeq0lem  24011  dgrcolem2  24075  geolim3  24139  aaliou3lem2  24143  aaliou3lem8  24145  ulmdvlem1  24199  radcnvlem1  24212  radcnvlem2  24213  dvradcnv  24220  pserulm  24221  pserdvlem2  24227  abelthlem2  24231  abelthlem5  24234  abelthlem7  24237  abelth2  24241  tangtx  24302  tanabsge  24303  tanord1  24328  argregt0  24401  argrege0  24402  argimgt0  24403  abslogle  24409  logcnlem4  24436  logtayllem  24450  abscxpbnd  24539  ang180lem2  24585  atanlogsublem  24687  atans2  24703  leibpi  24714  birthdaylem3  24725  cxplim  24743  cxp2limlem  24747  cxploglim2  24750  jensenlem2  24759  jensen  24760  amgmlem  24761  emcllem2  24768  emcllem4  24770  emcllem7  24773  zetacvg  24786  lgamgulmlem2  24801  lgamgulmlem5  24804  lgamcvg2  24826  ftalem5  24848  basellem4  24855  basellem6  24857  basellem8  24859  basellem9  24860  chtwordi  24927  chpwordi  24928  ppiwordi  24933  ppiub  24974  vmalelog  24975  chtlepsi  24976  chtleppi  24980  chtublem  24981  chtub  24982  chpub  24990  logfaclbnd  24992  logfacrlim  24994  dchrptlem3  25036  bcmono  25047  bclbnd  25050  bposlem1  25054  bposlem6  25059  bposlem9  25062  lgsqrlem4  25119  2lgslem1c  25163  chebbnd1lem1  25203  chebbnd1lem3  25205  chebbnd1  25206  chtppilimlem1  25207  vmadivsum  25216  rplogsumlem2  25219  dchrisumlema  25222  dchrisumlem3  25225  dchrmusum2  25228  dchrvmasumlem3  25233  dchrvmasumiflem1  25235  dchrisum0flblem1  25242  dchrisum0re  25247  dchrisum0lem2a  25251  mulogsumlem  25265  mulog2sumlem1  25268  mulog2sumlem2  25269  2vmadivsumlem  25274  selberg2lem  25284  selberg3lem1  25291  selberg4lem1  25294  pntrlog2bndlem3  25313  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntpbnd1  25320  pntlemc  25329  pntlemr  25336  pntlemk  25340  pntlemo  25341  abvcxp  25349  ostth2lem1  25352  padicabv  25364  ostth2lem2  25368  ostth2lem3  25369  ostth2lem4  25370  ostth2  25371  legso  25539  trgcopy  25741  eucrct2eupth  27223  nvmtri  27654  imsmetlem  27673  vacn  27677  nmcvcn  27678  smcnlem  27680  blometi  27786  ipblnfi  27839  minvecolem2  27859  hhssnv  28249  nmcoplbi  29015  nmopcoi  29082  nmopcoadji  29088  idleop  29118  cdj1i  29420  isoun  29607  xlt2addrd  29651  omndmul  29842  ogrpsub  29845  archirngz  29871  gsumle  29907  ofldchr  29942  pstmxmet  30068  nexple  30199  esumpmono  30269  esumcvg  30276  meascnbl  30410  omsmon  30488  omsmeas  30513  dstfrvinc  30666  hgt750lemd  30854  hgt750lema  30863  hgt750leme  30864  derangenlem  31279  subfaclefac  31284  subfaclim  31296  erdszelem10  31308  sinccvglem  31692  iprodefisum  31753  noextendlt  31947  noextendgt  31948  nosupbnd1  31985  nosupbnd2lem1  31986  unbdqndv2lem2  32626  itg2gt0cn  33595  ibladdnclem  33596  iblabsnc  33604  iblmulc2nc  33605  itgabsnc  33609  bddiblnc  33610  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  mettrifi  33683  equivbnd2  33721  heiborlem6  33745  bfplem1  33751  bfp  33753  rrnmet  33758  rrndstprj1  33759  rrndstprj2  33760  dalawlem3  35477  dalawlem4  35478  dalawlem6  35480  dalawlem9  35483  dalawlem11  35485  dalawlem12  35486  dalawlem15  35489  cdleme3c  35835  cdleme7e  35852  cdleme26e  35964  cdleme26eALTN  35966  cdleme27a  35972  cdleme32c  36048  cdleme32e  36050  cdleme32le  36052  cdlemg9b  36238  cdlemg12b  36249  cdlemg12d  36251  trlcolem  36331  trlcone  36333  cdlemk7  36453  cdlemk7u  36475  cdlemk39  36521  cdlemk11ta  36534  cdlemk11tc  36550  mapdcnvatN  37272  irrapxlem5  37707  pell1qrge1  37751  pell1qrgaplem  37754  pell14qrgapw  37757  pellqrex  37760  pellfund14  37779  expmordi  37829  jm2.17a  37844  jm2.17c  37846  acongeq  37867  jm2.19  37877  jm2.27a  37889  jm2.27c  37891  jm3.1lem2  37902  areaquad  38119  rp-isfinite6  38181  hashnzfzclim  38838  binomcxplemnotnn0  38872  absimlere  40023  monoord2xrv  40027  ltmod  40188  dvbdfbdioolem2  40462  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  stoweidlem3  40538  stoweidlem26  40561  wallispilem1  40600  wallispilem5  40604  stirlinglem1  40609  stirlinglem5  40613  stirlinglem8  40616  stirlinglem10  40618  stirlinglem12  40620  fourierdlem6  40648  fourierdlem7  40649  fourierdlem14  40656  fourierdlem19  40661  fourierdlem35  40677  fourierdlem39  40681  fourierdlem42  40684  fourierdlem50  40691  fourierdlem73  40714  fourierdlem76  40717  fourierdlem77  40718  fourierdlem81  40722  fourierdlem90  40731  fourierdlem92  40733  fourierdlem93  40734  fourierdlem111  40752  fouriersw  40766  etransclem38  40807  sge0split  40944  lighneallem4a  41850  rnghmsubcsetc  42302  rhmsubcsetc  42348  rhmsubcrngc  42354  rhmsubc  42415  rhmsubcALTV  42433  logbpw2m1  42686  dignn0flhalflem1  42734  dignn0flhalflem2  42735  amgmwlem  42876
  Copyright terms: Public domain W3C validator