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

Theorem breq12d 4185
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 4177 . 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 4172
This theorem is referenced by:  breq123d  4186  3brtr3d  4201  3brtr4d  4202  pocl  4470  cnvpo  5369  isoeq1  5998  isocnv  6009  isotr  6015  caovordig  6211  caovordg  6213  caovord2d  6215  caovord  6217  ofrfval  6272  ofrval  6274  ofrfval2  6282  caofref  6289  fnwelem  6420  fundmeng  7140  xpsneng  7152  xpcomeng  7159  xpdom2g  7163  map2xp  7236  mapdom3  7238  limensuc  7243  infensuc  7244  unxpdom  7275  pssnn  7286  dif1enOLD  7299  dif1en  7300  unfilem3  7332  unfi  7333  domunfican  7338  fodomfi  7344  marypha1lem  7396  wemaplem1  7471  wemaplem2  7472  wemapwe  7610  dif1card  7848  infxpenlem  7851  pwsdompw  8040  infmap2  8054  sornom  8113  isfin5  8135  isfin6  8136  domtriomlem  8278  axdc2lem  8284  axdclem2  8356  pwcfsdom  8414  cfpwsdom  8415  alephom  8416  fpwwe2lem7  8467  fpwwe2lem9  8469  pwxpndom2  8496  tskcard  8612  ordpipq  8775  adderpqlem  8787  mulerpqlem  8788  mulcanenq  8793  lterpq  8803  ltanq  8804  ltmnq  8805  ltaddnq  8807  ltrnq  8812  archnq  8813  reclem4pr  8883  ltasr  8931  sqgt0sr  8937  axpre-ltadd  8998  axpre-mulgt0  8999  ltadd1  9451  leadd2  9453  ltmul2  9817  lemul2  9819  lemul1a  9820  ltdiv1  9830  ltdiv2  9851  lediv2  9856  uzindOLD  10320  xleadd1  10790  xltadd2  10792  xsubge0  10796  xlemul1a  10823  xlemul1  10825  xlemul2  10826  xltmul2  10828  fzennn  11262  monoord  11308  monoord2  11309  ltexp2r  11391  leexp1a  11393  sqlecan  11442  bernneq  11460  faclbnd  11536  faclbnd3  11538  faclbnd4lem1  11539  faclbnd4lem2  11540  faclbnd4lem3  11541  faclbnd4lem4  11542  faclbnd6  11545  facubnd  11546  rlimcld2  12327  isercoll2  12417  climsup  12418  iseraltlem2  12431  fsumabs  12535  fsumrlim  12545  climcndslem1  12584  climcndslem2  12585  supcvg  12590  geomulcvg  12608  cvgrat  12615  ruclem2  12786  ruclem8  12791  sadcaddlem  12924  sadcadd  12925  nn0seqcvgd  13016  algcvg  13022  algcvga  13025  eucalgcvga  13032  isprm5  13067  qnumgt0  13097  pcprendvds2  13170  pcpremul  13172  pcadd2  13214  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  2expltfac  13381  xpsle  13761  mreexexlemd  13824  issubc  13990  latjlej2  14450  latmlem2  14466  sylow1lem3  15189  isslw  15197  fislw  15214  efgi  15306  lt6abl  15459  ablfac1eu  15586  isabv  15862  abvtri  15873  isucn  18261  ispsmet  18288  psmettri2  18293  ismet  18306  isxmet  18307  xmettri2  18323  imasdsf1olem  18356  imasf1oxmet  18358  blvalps  18368  blval  18369  comet  18496  stdbdxmet  18498  nrmmetd  18575  tngngp  18648  nmofval  18701  nmolb2d  18705  nmoi  18715  nmoix  18716  icopnfhmeo  18921  xrhmeo  18924  evth2  18938  pi1grplem  19027  minveclem6  19288  ovolfiniun  19350  ovoliunlem3  19353  voliunlem3  19399  ioombl1  19409  mbfmax  19494  mbfpos  19496  itg1climres  19559  mbfi1fseqlem2  19561  mbfi1fseqlem6  19565  mbfi1fseq  19566  mbfmullem  19570  itg2split  19594  itg2monolem1  19595  itg2monolem3  19597  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq  19600  itg2i1fseq2  19601  itg2addlem  19603  rolle  19827  dvlip  19830  c1lip1  19834  dvcnvrelem1  19854  dvcvx  19857  ply1divex  20012  q1pval  20029  fta1glem2  20042  fta1g  20043  fta1b  20045  plydivlem3  20165  fta1lem  20177  fta1  20178  aalioulem3  20204  aalioulem4  20205  aaliou3lem2  20213  aaliou3lem8  20215  aaliou3lem9  20220  ulmdvlem1  20269  ulmdvlem3  20271  abelthlem2  20301  abelthlem7a  20306  argrege0  20459  cxplt  20538  cxplea  20540  cxple2  20541  cxplt3  20544  rlimcxp  20765  scvxcvx  20777  jensenlem2  20779  ftalem3  20810  ftalem7  20814  vmalelog  20942  chtub  20949  chpchtsum  20956  bclbnd  21017  efexple  21018  bposlem5  21025  bposlem6  21026  bposlem7  21027  lgsdilem  21059  dchrisumlem3  21138  dchrmusumlema  21140  dchrmusum2  21141  dchrvmasumlem2  21145  dchrvmasumlema  21147  dchrvmasumiflem1  21148  dchrisum0flblem2  21156  dchrisum0flb  21157  dchrisum0lema  21161  dchrisum0lem1b  21162  dchrisum0lem2  21165  pntrlog2bndlem2  21225  pntibndlem2  21238  pntlemf  21252  ostth2lem1  21265  qabvle  21272  sizeusglecusg  21448  isnvlem  22042  nvtri  22112  nmlnoubi  22250  nmblolbii  22253  nmblolbi  22254  blocnilem  22258  sii  22308  ubthlem2  22326  minvecolem3  22331  minvecolem5  22336  minvecolem6  22337  norm-ii  22593  norm3dif  22605  norm3adifi  22608  bcs  22636  pjnorm  23179  pjnel  23181  nmbdoplbi  23480  nmbdoplb  23481  nmcoplb  23486  lnconi  23489  nmbdfnlb  23506  nmcfnlb  23510  pjdifnormi  23623  mdslmd2i  23786  cvmd  23792  cvexch  23830  cdj1i  23889  cdj3lem1  23890  cdj3lem2b  23893  cdj3lem3b  23896  cdj3i  23897  csbcnvg  23990  isoun  24042  isofld  24188  ofldadd  24191  isinftm  24204  pstmxmet  24245  xrmulc1cn  24269  lmdvg  24291  logblt  24359  faeval  24550  brfae  24552  sconpht  24869  snmlval  24971  lediv2aALT  25070  ntrivcvgtail  25181  faclim  25313  poseq  25467  sltval2  25524  sltres  25532  nodense  25557  nobndup  25568  nobnddown  25569  brbtwn2  25748  axlowdim  25804  fvtransport  25870  idinside  25922  btwnconn1lem7  25931  btwnconn1lem11  25935  btwnconn1lem12  25936  itg2addnclem  26155  itg2addnclem3  26157  itg2gt0cn  26159  dvreasin  26179  areacirclem2  26181  nn0prpwlem  26215  seqpo  26341  incsequz  26342  metf1o  26351  mettrifi  26353  cntotbnd  26395  heiborlem4  26413  heiborlem6  26415  heiborlem10  26419  bfplem1  26421  bfplem2  26422  irrapxlem2  26776  irrapxlem4  26778  irrapxlem5  26779  irrapxlem6  26780  pellexlem3  26784  monotuz  26894  monotoddzzfi  26895  monotoddzz  26896  expmordi  26900  jm2.17a  26915  jm2.17b  26916  rmygeid  26919  rmydioph  26975  expdiophlem1  26982  expdiophlem2  26983  ttac  26997  fnwe2lem2  27016  climinf  27599  climinff  27604  stoweidlem3  27619  sbcfun  27854  swrdccat3b  28031  isopos  29663  oplecon3b  29683  atlatle  29803  4at2  30096  pmaple  30243  islaut  30565  lautcnvle  30571  lautco  30579  ltrncnvel  30624  cdlemeg49lebilem  31021  cdlemg17h  31150  tendoset  31241  tendotp  31243  cdlemk39s  31421
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator