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

Theorem breq12d 4300
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Hypotheses
Ref Expression
breq1d.1  |-  ( ph  ->  A  =  B )
breq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
breq12d  |-  ( ph  ->  ( A R C  <-> 
B R D ) )

Proof of Theorem breq12d
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 breq12 4292 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   class class class wbr 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288
This theorem is referenced by:  breq123d  4301  3brtr3d  4316  3brtr4d  4317  sbcbr  4340  pocl  4643  csbcnvgALT  5019  cnvpo  5370  sbcfung  5436  isoeq1  6005  isocnv  6016  isotr  6022  caovordig  6263  caovordg  6265  caovord2d  6267  caovord  6269  ofrfval  6323  ofrval  6325  ofrfval2  6332  caofref  6341  fnwelem  6682  fundmeng  7376  xpsneng  7388  xpcomeng  7395  xpdom2g  7399  map2xp  7473  mapdom3  7475  limensuc  7480  infensuc  7481  unxpdom  7512  pssnn  7523  dif1enOLD  7536  dif1en  7537  unfilem3  7570  unfi  7571  domunfican  7576  fodomfi  7582  marypha1lem  7675  wemaplem1  7752  wemaplem2  7753  wemapwe  7920  wemapweOLD  7921  dif1card  8169  infxpenlem  8172  pwsdompw  8365  infmap2  8379  sornom  8438  isfin5  8460  isfin6  8461  domtriomlem  8603  axdc2lem  8609  axdclem2  8681  pwcfsdom  8739  cfpwsdom  8740  alephom  8741  fpwwe2lem7  8795  fpwwe2lem9  8797  pwxpndom2  8824  tskcard  8940  ordpipq  9103  adderpqlem  9115  mulerpqlem  9116  mulcanenq  9121  lterpq  9131  ltanq  9132  ltmnq  9133  ltaddnq  9135  ltrnq  9140  archnq  9141  reclem4pr  9211  ltasr  9259  sqgt0sr  9265  axpre-ltadd  9326  axpre-mulgt0  9327  ltadd1  9798  leadd2  9800  ltmul2  10172  lemul2  10174  lemul1a  10175  ltdiv1  10185  ltdiv2  10209  lediv2  10214  uzindOLD  10728  xleadd1  11210  xltadd2  11212  xsubge0  11216  xlemul1a  11243  xlemul1  11245  xlemul2  11246  xltmul2  11248  ltdifltdiv  11670  fzennn  11782  monoord  11828  monoord2  11829  ltexp2r  11912  leexp1a  11914  sqlecan  11964  bernneq  11982  faclbnd  12058  faclbnd3  12060  faclbnd4lem1  12061  faclbnd4lem2  12062  faclbnd4lem3  12063  faclbnd4lem4  12064  faclbnd6  12067  facubnd  12068  rlimcld2  13048  isercoll2  13138  climsup  13139  iseraltlem2  13152  fsumabs  13256  fsumrlim  13266  climcndslem1  13304  climcndslem2  13305  supcvg  13310  geomulcvg  13328  cvgrat  13335  ruclem2  13506  ruclem8  13511  sadcaddlem  13645  sadcadd  13646  nn0seqcvgd  13737  algcvg  13743  algcvga  13746  eucalgcvga  13753  isprm5  13790  qnumgt0  13820  pcprendvds2  13900  pcpremul  13902  pcadd2  13944  prmreclem4  13972  prmreclem5  13973  prmreclem6  13974  2expltfac  14111  xpsle  14511  mreexexlemd  14574  issubc  14740  latjlej2  15228  latmlem2  15244  sylow1lem3  16090  isslw  16098  fislw  16115  efgi  16207  lt6abl  16362  ablfac1eu  16562  isabv  16882  abvtri  16893  isucn  19828  ispsmet  19855  psmettri2  19860  ismet  19873  isxmet  19874  xmettri2  19890  imasdsf1olem  19923  imasf1oxmet  19925  blvalps  19935  blval  19936  comet  20063  stdbdxmet  20065  nrmmetd  20142  tngngp  20215  nmofval  20268  nmolb2d  20272  nmoi  20282  nmoix  20283  icopnfhmeo  20490  xrhmeo  20493  evth2  20507  pi1grplem  20596  minveclem6  20896  ovolfiniun  20959  ovoliunlem3  20962  voliunlem3  21008  ioombl1  21018  mbfmax  21102  mbfpos  21104  itg1climres  21167  mbfi1fseqlem2  21169  mbfi1fseqlem6  21173  mbfi1fseq  21174  mbfmullem  21178  itg2split  21202  itg2monolem1  21203  itg2monolem3  21205  itg2mono  21206  itg2i1fseqle  21207  itg2i1fseq  21208  itg2i1fseq2  21209  itg2addlem  21211  rolle  21437  dvlip  21440  c1lip1  21444  dvcnvrelem1  21464  dvcvx  21467  ply1divex  21583  q1pval  21600  fta1glem2  21613  fta1g  21614  fta1b  21616  plydivlem3  21736  fta1lem  21748  fta1  21749  aalioulem3  21775  aalioulem4  21776  aaliou3lem2  21784  aaliou3lem8  21786  aaliou3lem9  21791  ulmdvlem1  21840  ulmdvlem3  21842  abelthlem2  21872  abelthlem7a  21877  argrege0  22035  cxplt  22114  cxplea  22116  cxple2  22117  cxplt3  22120  rlimcxp  22342  scvxcvx  22354  jensenlem2  22356  ftalem3  22387  ftalem7  22391  vmalelog  22519  chtub  22526  chpchtsum  22533  bclbnd  22594  efexple  22595  bposlem5  22602  bposlem6  22603  bposlem7  22604  lgsdilem  22636  dchrisumlem3  22715  dchrmusumlema  22717  dchrmusum2  22718  dchrvmasumlem2  22722  dchrvmasumlema  22724  dchrvmasumiflem1  22725  dchrisum0flblem2  22733  dchrisum0flb  22734  dchrisum0lema  22738  dchrisum0lem1b  22739  dchrisum0lem2  22742  pntrlog2bndlem2  22802  pntibndlem2  22815  pntlemf  22829  ostth2lem1  22842  qabvle  22849  brbtwn2  23102  axlowdim  23158  sizeusglecusg  23345  isnvlem  23939  nvtri  24009  nmlnoubi  24147  nmblolbii  24150  nmblolbi  24151  blocnilem  24155  sii  24205  ubthlem2  24223  minvecolem3  24228  minvecolem5  24233  minvecolem6  24234  norm-ii  24491  norm3dif  24503  norm3adifi  24506  bcs  24534  pjnorm  25078  pjnel  25080  nmbdoplbi  25379  nmbdoplb  25380  nmcoplb  25385  lnconi  25388  nmbdfnlb  25405  nmcfnlb  25409  pjdifnormi  25522  mdslmd2i  25685  cvmd  25691  cvexch  25729  cdj1i  25788  cdj3lem1  25789  cdj3lem2b  25792  cdj3lem3b  25795  cdj3i  25796  isoun  25948  mul2lt0rlt0  25989  isomnd  26115  omndadd  26120  omndmul  26128  ogrpaddltbi  26133  ogrpinvlt  26138  isinftm  26149  archiabllem2b  26164  gsumle  26197  pstmxmet  26276  xrmulc1cn  26312  lmdvg  26335  nexple  26400  logblt  26417  faeval  26614  brfae  26616  sconpht  27070  snmlval  27172  lediv2aALT  27273  ntrivcvgtail  27366  faclim  27503  poseq  27665  sltval2  27748  sltres  27756  nodense  27781  nobndup  27792  nobnddown  27793  fvtransport  28014  idinside  28066  btwnconn1lem7  28075  btwnconn1lem11  28079  btwnconn1lem12  28080  heicant  28379  itg2addnclem  28396  itg2addnclem3  28398  itg2gt0cn  28400  ftc1anclem6  28425  ftc1anc  28428  ftc2nc  28429  dvasin  28433  areacirclem1  28437  nn0prpwlem  28470  seqpo  28596  incsequz  28597  metf1o  28604  mettrifi  28606  cntotbnd  28648  heiborlem4  28666  heiborlem6  28668  heiborlem10  28672  bfplem1  28674  bfplem2  28675  irrapxlem2  29117  irrapxlem4  29119  irrapxlem5  29120  irrapxlem6  29121  pellexlem3  29125  monotuz  29235  monotoddzzfi  29236  monotoddzz  29237  expmordi  29241  jm2.17a  29256  jm2.17b  29257  rmygeid  29260  rmydioph  29316  expdiophlem1  29323  expdiophlem2  29324  ttac  29338  fnwe2lem2  29357  climinf  29732  climinff  29737  stoweidlem3  29751  2elfz2melfz  30155  isrusgra  30497  extwwlkfablem2  30624  lindslinindsimp2lem5  30885  isopos  32665  oplecon3b  32685  atlatle  32805  4at2  33098  pmaple  33245  islaut  33567  lautcnvle  33573  lautco  33581  ltrncnvel  33626  cdlemeg49lebilem  34023  cdlemg17h  34152  tendoset  34243  tendotp  34245  cdlemk39s  34423
  Copyright terms: Public domain W3C validator