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

Theorem breq12d 4159
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 4151 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   class class class wbr 4146
This theorem is referenced by:  breq123d  4160  3brtr3d  4175  3brtr4d  4176  pocl  4444  cnvpo  5343  isoeq1  5971  isocnv  5982  isotr  5988  caovordig  6184  caovordg  6186  caovord2d  6188  caovord  6190  ofrfval  6245  ofrval  6247  ofrfval2  6255  caofref  6262  fnwelem  6390  fundmeng  7110  xpsneng  7122  xpcomeng  7129  xpdom2g  7133  map2xp  7206  mapdom3  7208  limensuc  7213  infensuc  7214  unxpdom  7245  pssnn  7256  dif1enOLD  7269  dif1en  7270  unfilem3  7302  unfi  7303  domunfican  7308  fodomfi  7314  marypha1lem  7366  wemaplem1  7441  wemaplem2  7442  wemapwe  7580  dif1card  7818  infxpenlem  7821  pwsdompw  8010  infmap2  8024  sornom  8083  isfin5  8105  isfin6  8106  domtriomlem  8248  axdc2lem  8254  axdclem2  8326  pwcfsdom  8384  cfpwsdom  8385  alephom  8386  fpwwe2lem7  8437  fpwwe2lem9  8439  pwxpndom2  8466  tskcard  8582  ordpipq  8745  adderpqlem  8757  mulerpqlem  8758  mulcanenq  8763  lterpq  8773  ltanq  8774  ltmnq  8775  ltaddnq  8777  ltrnq  8782  archnq  8783  reclem4pr  8853  ltasr  8901  sqgt0sr  8907  axpre-ltadd  8968  axpre-mulgt0  8969  ltadd1  9420  leadd2  9422  ltmul2  9786  lemul2  9788  lemul1a  9789  ltdiv1  9799  ltdiv2  9820  lediv2  9825  uzindOLD  10289  xleadd1  10759  xltadd2  10761  xsubge0  10765  xlemul1a  10792  xlemul1  10794  xlemul2  10795  xltmul2  10797  fzennn  11227  monoord  11273  monoord2  11274  ltexp2r  11356  leexp1a  11358  sqlecan  11407  bernneq  11425  faclbnd  11501  faclbnd3  11503  faclbnd4lem1  11504  faclbnd4lem2  11505  faclbnd4lem3  11506  faclbnd4lem4  11507  faclbnd6  11510  facubnd  11511  rlimcld2  12292  isercoll2  12382  climsup  12383  iseraltlem2  12396  fsumabs  12500  fsumrlim  12510  climcndslem1  12549  climcndslem2  12550  supcvg  12555  geomulcvg  12573  cvgrat  12580  ruclem2  12751  ruclem8  12756  sadcaddlem  12889  sadcadd  12890  nn0seqcvgd  12981  algcvg  12987  algcvga  12990  eucalgcvga  12997  isprm5  13032  qnumgt0  13062  pcprendvds2  13135  pcpremul  13137  pcadd2  13179  prmreclem4  13207  prmreclem5  13208  prmreclem6  13209  2expltfac  13346  xpsle  13726  mreexexlemd  13789  issubc  13955  latjlej2  14415  latmlem2  14431  sylow1lem3  15154  isslw  15162  fislw  15179  efgi  15271  lt6abl  15424  ablfac1eu  15551  isabv  15827  abvtri  15838  isucn  18222  ismet  18255  isxmet  18256  xmettri2  18272  imasdsf1olem  18304  imasf1oxmet  18306  blval  18315  comet  18426  stdbdxmet  18428  nrmmetd  18486  tngngp  18559  nmofval  18612  nmolb2d  18616  nmoi  18626  nmoix  18627  icopnfhmeo  18832  xrhmeo  18835  evth2  18849  pi1grplem  18938  minveclem6  19195  ovolfiniun  19257  ovoliunlem3  19260  voliunlem3  19306  ioombl1  19316  mbfmax  19401  mbfpos  19403  itg1climres  19466  mbfi1fseqlem2  19468  mbfi1fseqlem6  19472  mbfi1fseq  19473  mbfmullem  19477  itg2split  19501  itg2monolem1  19502  itg2monolem3  19504  itg2mono  19505  itg2i1fseqle  19506  itg2i1fseq  19507  itg2i1fseq2  19508  itg2addlem  19510  rolle  19734  dvlip  19737  c1lip1  19741  dvcnvrelem1  19761  dvcvx  19764  ply1divex  19919  q1pval  19936  fta1glem2  19949  fta1g  19950  fta1b  19952  plydivlem3  20072  fta1lem  20084  fta1  20085  aalioulem3  20111  aalioulem4  20112  aaliou3lem2  20120  aaliou3lem8  20122  aaliou3lem9  20127  ulmdvlem1  20176  ulmdvlem3  20178  abelthlem2  20208  abelthlem7a  20213  argrege0  20366  cxplt  20445  cxplea  20447  cxple2  20448  cxplt3  20451  rlimcxp  20672  scvxcvx  20684  jensenlem2  20686  ftalem3  20717  ftalem7  20721  vmalelog  20849  chtub  20856  chpchtsum  20863  bclbnd  20924  efexple  20925  bposlem5  20932  bposlem6  20933  bposlem7  20934  lgsdilem  20966  dchrisumlem3  21045  dchrmusumlema  21047  dchrmusum2  21048  dchrvmasumlem2  21052  dchrvmasumlema  21054  dchrvmasumiflem1  21055  dchrisum0flblem2  21063  dchrisum0flb  21064  dchrisum0lema  21068  dchrisum0lem1b  21069  dchrisum0lem2  21072  pntrlog2bndlem2  21132  pntibndlem2  21145  pntlemf  21159  ostth2lem1  21172  qabvle  21179  sizeusglecusg  21354  isnvlem  21930  nvtri  22000  nmlnoubi  22138  nmblolbii  22141  nmblolbi  22142  blocnilem  22146  sii  22196  ubthlem2  22214  minvecolem3  22219  minvecolem5  22224  minvecolem6  22225  norm-ii  22481  norm3dif  22493  norm3adifi  22496  bcs  22524  pjnorm  23067  pjnel  23069  nmbdoplbi  23368  nmbdoplb  23369  nmcoplb  23374  lnconi  23377  nmbdfnlb  23394  nmcfnlb  23398  pjdifnormi  23511  mdslmd2i  23674  cvmd  23680  cvexch  23718  cdj1i  23777  cdj3lem1  23778  cdj3lem2b  23781  cdj3lem3b  23784  cdj3i  23785  csbcnvg  23873  isoun  23923  isofld  24054  ofldadd  24057  xrmulc1cn  24113  lmdvg  24135  logblt  24195  faeval  24384  brfae  24386  sconpht  24688  snmlval  24790  lediv2aALT  24889  ntrivcvgtail  25000  faclim  25116  poseq  25270  sltval2  25327  sltres  25335  nodense  25360  nobndup  25371  nobnddown  25372  brbtwn2  25551  axlowdim  25607  fvtransport  25673  idinside  25725  btwnconn1lem7  25734  btwnconn1lem11  25738  btwnconn1lem12  25739  itg2addnclem  25950  itg2addnc  25952  itg2gt0cn  25953  dvreasin  25973  areacirclem2  25975  nn0prpwlem  26009  seqpo  26135  incsequz  26136  metf1o  26145  mettrifi  26147  cntotbnd  26189  heiborlem4  26207  heiborlem6  26209  heiborlem10  26213  bfplem1  26215  bfplem2  26216  irrapxlem2  26570  irrapxlem4  26572  irrapxlem5  26573  irrapxlem6  26574  pellexlem3  26578  monotuz  26688  monotoddzzfi  26689  monotoddzz  26690  expmordi  26694  jm2.17a  26709  jm2.17b  26710  rmygeid  26713  rmydioph  26769  expdiophlem1  26776  expdiophlem2  26777  ttac  26791  fnwe2lem2  26810  climinf  27393  climinff  27398  stoweidlem3  27413  sbcfun  27648  isopos  29346  oplecon3b  29366  atlatle  29486  4at2  29779  pmaple  29926  islaut  30248  lautcnvle  30254  lautco  30262  ltrncnvel  30307  cdlemeg49lebilem  30704  cdlemg17h  30833  tendoset  30924  tendotp  30926  cdlemk39s  31104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-br 4147
  Copyright terms: Public domain W3C validator