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

Theorem breq12d 4036
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 4028 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  breq123d  4037  3brtr3d  4052  3brtr4d  4053  pocl  4321  cnvpo  5213  isoeq1  5816  isocnv  5827  isotr  5833  caovordig  6025  caovordg  6027  caovord2d  6029  caovord  6031  ofrfval  6086  ofrval  6088  ofrfval2  6096  caofref  6103  fnwelem  6230  fundmeng  6935  xpsneng  6947  xpcomeng  6954  xpdom2g  6958  map2xp  7031  mapdom3  7033  limensuc  7038  infensuc  7039  unxpdom  7070  pssnn  7081  dif1enOLD  7090  dif1en  7091  unfilem3  7123  unfi  7124  domunfican  7129  fodomfi  7135  marypha1lem  7186  wemaplem1  7261  wemaplem2  7262  wemapwe  7400  dif1card  7638  infxpenlem  7641  pwsdompw  7830  infmap2  7844  sornom  7903  isfin5  7925  isfin6  7926  domtriomlem  8068  axdc2lem  8074  axdclem2  8147  pwcfsdom  8205  cfpwsdom  8206  alephom  8207  fpwwe2lem7  8258  fpwwe2lem9  8260  pwxpndom2  8287  tskcard  8403  ordpipq  8566  adderpqlem  8578  mulerpqlem  8579  mulcanenq  8584  lterpq  8594  ltanq  8595  ltmnq  8596  ltaddnq  8598  ltrnq  8603  archnq  8604  reclem4pr  8674  ltasr  8722  sqgt0sr  8728  axpre-ltadd  8789  axpre-mulgt0  8790  ltadd1  9241  leadd2  9243  ltmul2  9607  lemul2  9609  lemul1a  9610  ltdiv1  9620  ltdiv2  9641  lediv2  9646  uzindOLD  10106  xleadd1  10575  xltadd2  10577  xsubge0  10581  xlemul1a  10608  xlemul1  10610  xlemul2  10611  xltmul2  10613  fzennn  11030  monoord  11076  monoord2  11077  ltexp2r  11158  leexp1a  11160  sqlecan  11209  bernneq  11227  faclbnd  11303  faclbnd3  11305  faclbnd4lem1  11306  faclbnd4lem2  11307  faclbnd4lem3  11308  faclbnd4lem4  11309  faclbnd6  11312  facubnd  11313  rlimcld2  12052  isercoll2  12142  climsup  12143  iseraltlem2  12155  fsumabs  12259  fsumrlim  12269  climcndslem1  12308  climcndslem2  12309  supcvg  12314  geomulcvg  12332  cvgrat  12339  ruclem2  12510  ruclem8  12515  sadcaddlem  12648  sadcadd  12649  nn0seqcvgd  12740  algcvg  12746  algcvga  12749  eucalgcvga  12756  isprm5  12791  qnumgt0  12821  pcprendvds2  12894  pcpremul  12896  pcadd2  12938  prmreclem4  12966  prmreclem5  12967  prmreclem6  12968  2expltfac  13105  xpsle  13483  mreexexlemd  13546  issubc  13712  latjlej2  14172  latmlem2  14188  sylow1lem3  14911  isslw  14919  fislw  14936  efgi  15028  lt6abl  15181  ablfac1eu  15308  isabv  15584  abvtri  15595  ismet  17888  isxmet  17889  xmettri2  17905  imasdsf1olem  17937  imasf1oxmet  17939  blval  17948  comet  18059  stdbdxmet  18061  nrmmetd  18097  tngngp  18170  nmofval  18223  nmolb2d  18227  nmoi  18237  nmoix  18238  icopnfhmeo  18441  xrhmeo  18444  evth2  18458  pi1grplem  18547  minveclem6  18798  ovolfiniun  18860  ovoliunlem3  18863  voliunlem3  18909  ioombl1  18919  mbfmax  19004  mbfpos  19006  itg1climres  19069  mbfi1fseqlem2  19071  mbfi1fseqlem6  19075  mbfi1fseq  19076  mbfmullem  19080  itg2split  19104  itg2monolem1  19105  itg2monolem3  19107  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq  19110  itg2i1fseq2  19111  itg2addlem  19113  rolle  19337  dvlip  19340  c1lip1  19344  dvcnvrelem1  19364  dvcvx  19367  ply1divex  19522  q1pval  19539  fta1glem2  19552  fta1g  19553  fta1b  19555  plydivlem3  19675  fta1lem  19687  fta1  19688  aalioulem3  19714  aalioulem4  19715  aaliou3lem2  19723  aaliou3lem8  19725  aaliou3lem9  19730  ulmdvlem1  19777  ulmdvlem3  19779  abelthlem2  19808  abelthlem7a  19813  argrege0  19965  cxplt  20041  cxplea  20043  cxple2  20044  cxplt3  20047  rlimcxp  20268  scvxcvx  20280  jensenlem2  20282  ftalem3  20312  ftalem7  20316  vmalelog  20444  chtub  20451  chpchtsum  20458  bclbnd  20519  efexple  20520  bposlem5  20527  bposlem6  20528  bposlem7  20529  lgsdilem  20561  dchrisumlem3  20640  dchrmusumlema  20642  dchrmusum2  20643  dchrvmasumlem2  20647  dchrvmasumlema  20649  dchrvmasumiflem1  20650  dchrisum0flblem2  20658  dchrisum0flb  20659  dchrisum0lema  20663  dchrisum0lem1b  20664  dchrisum0lem2  20667  pntrlog2bndlem2  20727  pntibndlem2  20740  pntlemf  20754  ostth2lem1  20767  qabvle  20774  isnvlem  21166  nvtri  21236  nmlnoubi  21374  nmblolbii  21377  nmblolbi  21378  blocnilem  21382  sii  21432  ubthlem2  21450  minvecolem3  21455  minvecolem5  21460  minvecolem6  21461  norm-ii  21717  norm3dif  21729  norm3adifi  21732  bcs  21760  pjnorm  22303  pjnel  22305  nmbdoplbi  22604  nmbdoplb  22605  nmcoplb  22610  lnconi  22613  nmbdfnlb  22630  nmcfnlb  22634  pjdifnormi  22747  mdslmd2i  22910  cvmd  22916  cvexch  22954  cdj1i  23013  cdj3lem1  23014  cdj3lem2b  23017  cdj3lem3b  23020  cdj3i  23021  csbcnvg  23198  isoun  23242  xrmulc1cn  23303  xrge0iifiso  23317  lmdvg  23376  logblt  23408  meascnbl  23546  dstfrvclim1  23678  sconpht  23760  snmlval  23914  lediv2aALT  24013  poseq  24253  sltval2  24310  sltres  24318  nodense  24343  nobndup  24354  nobnddown  24355  brbtwn2  24533  axlowdim  24589  fvtransport  24655  idinside  24707  btwnconn1lem7  24716  btwnconn1lem11  24720  btwnconn1lem12  24721  dvreasin  24923  areacirclem2  24925  domintreflemb  25062  domintrefc  25125  isoriso2  25213  oriso  25214  preotr2  25235  isibcg  26191  nn0prpwlem  26238  seqpo  26457  incsequz  26458  metf1o  26469  mettrifi  26473  cntotbnd  26520  heiborlem4  26538  heiborlem6  26540  heiborlem10  26544  bfplem1  26546  bfplem2  26547  irrapxlem2  26908  irrapxlem4  26910  irrapxlem5  26911  irrapxlem6  26912  pellexlem3  26916  monotuz  27026  monotoddzzfi  27027  monotoddzz  27028  expmordi  27032  jm2.17a  27047  jm2.17b  27048  rmygeid  27051  rmydioph  27107  expdiophlem1  27114  expdiophlem2  27115  ttac  27129  fnwe2lem2  27148  climinf  27732  climinff  27737  stoweidlem3  27752  sbcfun  27985  isopos  29370  oplecon3b  29390  atlatle  29510  4at2  29803  pmaple  29950  islaut  30272  lautcnvle  30278  lautco  30286  ltrncnvel  30331  cdlemeg49lebilem  30728  cdlemg17h  30857  tendoset  30948  tendotp  30950  cdlemk39s  31128
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator