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

Theorem breq12d 4052
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 4044 . 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 1632   class class class wbr 4039
This theorem is referenced by:  breq123d  4053  3brtr3d  4068  3brtr4d  4069  pocl  4337  cnvpo  5229  isoeq1  5832  isocnv  5843  isotr  5849  caovordig  6041  caovordg  6043  caovord2d  6045  caovord  6047  ofrfval  6102  ofrval  6104  ofrfval2  6112  caofref  6119  fnwelem  6246  fundmeng  6951  xpsneng  6963  xpcomeng  6970  xpdom2g  6974  map2xp  7047  mapdom3  7049  limensuc  7054  infensuc  7055  unxpdom  7086  pssnn  7097  dif1enOLD  7106  dif1en  7107  unfilem3  7139  unfi  7140  domunfican  7145  fodomfi  7151  marypha1lem  7202  wemaplem1  7277  wemaplem2  7278  wemapwe  7416  dif1card  7654  infxpenlem  7657  pwsdompw  7846  infmap2  7860  sornom  7919  isfin5  7941  isfin6  7942  domtriomlem  8084  axdc2lem  8090  axdclem2  8163  pwcfsdom  8221  cfpwsdom  8222  alephom  8223  fpwwe2lem7  8274  fpwwe2lem9  8276  pwxpndom2  8303  tskcard  8419  ordpipq  8582  adderpqlem  8594  mulerpqlem  8595  mulcanenq  8600  lterpq  8610  ltanq  8611  ltmnq  8612  ltaddnq  8614  ltrnq  8619  archnq  8620  reclem4pr  8690  ltasr  8738  sqgt0sr  8744  axpre-ltadd  8805  axpre-mulgt0  8806  ltadd1  9257  leadd2  9259  ltmul2  9623  lemul2  9625  lemul1a  9626  ltdiv1  9636  ltdiv2  9657  lediv2  9662  uzindOLD  10122  xleadd1  10591  xltadd2  10593  xsubge0  10597  xlemul1a  10624  xlemul1  10626  xlemul2  10627  xltmul2  10629  fzennn  11046  monoord  11092  monoord2  11093  ltexp2r  11174  leexp1a  11176  sqlecan  11225  bernneq  11243  faclbnd  11319  faclbnd3  11321  faclbnd4lem1  11322  faclbnd4lem2  11323  faclbnd4lem3  11324  faclbnd4lem4  11325  faclbnd6  11328  facubnd  11329  rlimcld2  12068  isercoll2  12158  climsup  12159  iseraltlem2  12171  fsumabs  12275  fsumrlim  12285  climcndslem1  12324  climcndslem2  12325  supcvg  12330  geomulcvg  12348  cvgrat  12355  ruclem2  12526  ruclem8  12531  sadcaddlem  12664  sadcadd  12665  nn0seqcvgd  12756  algcvg  12762  algcvga  12765  eucalgcvga  12772  isprm5  12807  qnumgt0  12837  pcprendvds2  12910  pcpremul  12912  pcadd2  12954  prmreclem4  12982  prmreclem5  12983  prmreclem6  12984  2expltfac  13121  xpsle  13499  mreexexlemd  13562  issubc  13728  latjlej2  14188  latmlem2  14204  sylow1lem3  14927  isslw  14935  fislw  14952  efgi  15044  lt6abl  15197  ablfac1eu  15324  isabv  15600  abvtri  15611  ismet  17904  isxmet  17905  xmettri2  17921  imasdsf1olem  17953  imasf1oxmet  17955  blval  17964  comet  18075  stdbdxmet  18077  nrmmetd  18113  tngngp  18186  nmofval  18239  nmolb2d  18243  nmoi  18253  nmoix  18254  icopnfhmeo  18457  xrhmeo  18460  evth2  18474  pi1grplem  18563  minveclem6  18814  ovolfiniun  18876  ovoliunlem3  18879  voliunlem3  18925  ioombl1  18935  mbfmax  19020  mbfpos  19022  itg1climres  19085  mbfi1fseqlem2  19087  mbfi1fseqlem6  19091  mbfi1fseq  19092  mbfmullem  19096  itg2split  19120  itg2monolem1  19121  itg2monolem3  19123  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq  19126  itg2i1fseq2  19127  itg2addlem  19129  rolle  19353  dvlip  19356  c1lip1  19360  dvcnvrelem1  19380  dvcvx  19383  ply1divex  19538  q1pval  19555  fta1glem2  19568  fta1g  19569  fta1b  19571  plydivlem3  19691  fta1lem  19703  fta1  19704  aalioulem3  19730  aalioulem4  19731  aaliou3lem2  19739  aaliou3lem8  19741  aaliou3lem9  19746  ulmdvlem1  19793  ulmdvlem3  19795  abelthlem2  19824  abelthlem7a  19829  argrege0  19981  cxplt  20057  cxplea  20059  cxple2  20060  cxplt3  20063  rlimcxp  20284  scvxcvx  20296  jensenlem2  20298  ftalem3  20328  ftalem7  20332  vmalelog  20460  chtub  20467  chpchtsum  20474  bclbnd  20535  efexple  20536  bposlem5  20543  bposlem6  20544  bposlem7  20545  lgsdilem  20577  dchrisumlem3  20656  dchrmusumlema  20658  dchrmusum2  20659  dchrvmasumlem2  20663  dchrvmasumlema  20665  dchrvmasumiflem1  20666  dchrisum0flblem2  20674  dchrisum0flb  20675  dchrisum0lema  20679  dchrisum0lem1b  20680  dchrisum0lem2  20683  pntrlog2bndlem2  20743  pntibndlem2  20756  pntlemf  20770  ostth2lem1  20783  qabvle  20790  isnvlem  21182  nvtri  21252  nmlnoubi  21390  nmblolbii  21393  nmblolbi  21394  blocnilem  21398  sii  21448  ubthlem2  21466  minvecolem3  21471  minvecolem5  21476  minvecolem6  21477  norm-ii  21733  norm3dif  21745  norm3adifi  21748  bcs  21776  pjnorm  22319  pjnel  22321  nmbdoplbi  22620  nmbdoplb  22621  nmcoplb  22626  lnconi  22629  nmbdfnlb  22646  nmcfnlb  22650  pjdifnormi  22763  mdslmd2i  22926  cvmd  22932  cvexch  22970  cdj1i  23029  cdj3lem1  23030  cdj3lem2b  23033  cdj3lem3b  23036  cdj3i  23037  csbcnvg  23213  isoun  23257  xrmulc1cn  23318  xrge0iifiso  23332  lmdvg  23391  logblt  23423  meascnbl  23561  dstfrvclim1  23693  sconpht  23775  snmlval  23929  lediv2aALT  24028  faclim  24126  poseq  24324  sltval2  24381  sltres  24389  nodense  24414  nobndup  24425  nobnddown  24426  brbtwn2  24605  axlowdim  24661  fvtransport  24727  idinside  24779  btwnconn1lem7  24788  btwnconn1lem11  24792  btwnconn1lem12  24793  itg2addnclem  25003  itg2addnc  25005  itg2gt0cn  25006  dvreasin  25026  areacirclem2  25028  domintreflemb  25165  domintrefc  25228  isoriso2  25316  oriso  25317  preotr2  25338  isibcg  26294  nn0prpwlem  26341  seqpo  26560  incsequz  26561  metf1o  26572  mettrifi  26576  cntotbnd  26623  heiborlem4  26641  heiborlem6  26643  heiborlem10  26647  bfplem1  26649  bfplem2  26650  irrapxlem2  27011  irrapxlem4  27013  irrapxlem5  27014  irrapxlem6  27015  pellexlem3  27019  monotuz  27129  monotoddzzfi  27130  monotoddzz  27131  expmordi  27135  jm2.17a  27150  jm2.17b  27151  rmygeid  27154  rmydioph  27210  expdiophlem1  27217  expdiophlem2  27218  ttac  27232  fnwe2lem2  27251  climinf  27835  climinff  27840  stoweidlem3  27855  sbcfun  28090  isopos  29992  oplecon3b  30012  atlatle  30132  4at2  30425  pmaple  30572  islaut  30894  lautcnvle  30900  lautco  30908  ltrncnvel  30953  cdlemeg49lebilem  31350  cdlemg17h  31479  tendoset  31570  tendotp  31572  cdlemk39s  31750
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator