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

Theorem breq12d 4380
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 4372 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 659 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1399   class class class wbr 4367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368
This theorem is referenced by:  breq123d  4381  3brtr3d  4396  3brtr4d  4397  sbcbr  4419  pocl  4721  csbcnvgALT  5100  cnvpo  5454  sbcfung  5519  isoeq1  6116  isocnv  6127  isotr  6133  caovordig  6379  caovordg  6381  caovord2d  6383  caovord  6385  ofrfval  6447  ofrval  6449  ofrfval2  6456  caofref  6465  fnwelem  6814  fundmeng  7509  xpsneng  7521  xpcomeng  7528  xpdom2g  7532  map2xp  7606  mapdom3  7608  limensuc  7613  infensuc  7614  unxpdom  7643  pssnn  7654  dif1en  7668  unfilem3  7701  unfi  7702  domunfican  7708  fodomfi  7714  marypha1lem  7808  wemaplem1  7886  wemaplem2  7887  wemapwe  8052  wemapweOLD  8053  dif1card  8301  infxpenlem  8304  pwsdompw  8497  infmap2  8511  sornom  8570  isfin5  8592  isfin6  8593  domtriomlem  8735  axdc2lem  8741  axdclem2  8813  pwcfsdom  8871  cfpwsdom  8872  alephom  8873  fpwwe2lem7  8925  fpwwe2lem9  8927  pwxpndom2  8954  tskcard  9070  ordpipq  9231  adderpqlem  9243  mulerpqlem  9244  mulcanenq  9249  lterpq  9259  ltanq  9260  ltmnq  9261  ltaddnq  9263  ltrnq  9268  archnq  9269  reclem4pr  9339  ltasr  9388  sqgt0sr  9394  axpre-ltadd  9455  axpre-mulgt0  9456  ltadd1  9937  leadd2  9939  ltmul2  10310  lemul2  10312  lemul1a  10313  ltdiv1  10323  ltdiv2  10346  lediv2  10351  xleadd1  11368  xltadd2  11370  xsubge0  11374  xlemul1a  11401  xlemul1  11403  xlemul2  11404  xltmul2  11406  ltdifltdiv  11866  fzennn  11981  monoord  12040  monoord2  12041  ltexp2r  12125  leexp1a  12127  sqlecan  12177  bernneq  12194  faclbnd  12270  faclbnd3  12272  faclbnd4lem1  12273  faclbnd4lem2  12274  faclbnd4lem3  12275  faclbnd4lem4  12276  faclbnd6  12279  facubnd  12280  rlimcld2  13403  isercoll2  13493  climsup  13494  iseraltlem2  13507  fsumabs  13617  fsumrlim  13627  climcndslem1  13663  climcndslem2  13664  supcvg  13669  geomulcvg  13687  cvgrat  13694  ntrivcvgtail  13711  ruclem2  13967  ruclem8  13972  sadcaddlem  14109  sadcadd  14110  nn0seqcvgd  14201  algcvg  14207  algcvga  14210  eucalgcvga  14217  isprm5  14255  qnumgt0  14285  pcprendvds2  14367  pcpremul  14369  pcadd2  14411  prmreclem4  14439  prmreclem5  14440  prmreclem6  14441  2expltfac  14579  xpsle  14988  mreexexlemd  15051  issubc  15241  latjlej2  15813  latmlem2  15829  sylow1lem3  16737  isslw  16745  fislw  16762  efgi  16854  lt6abl  17014  ablfac1eu  17237  isabv  17581  abvtri  17592  cayleyhamilton1  19478  isucn  20866  ispsmet  20893  psmettri2  20898  ismet  20911  isxmet  20912  xmettri2  20928  imasdsf1olem  20961  imasf1oxmet  20963  blvalps  20973  blval  20974  comet  21101  stdbdxmet  21103  nrmmetd  21180  tngngp  21253  nmofval  21306  nmolb2d  21310  nmoi  21320  nmoix  21321  icopnfhmeo  21528  xrhmeo  21531  evth2  21545  pi1grplem  21634  minveclem6  21934  ovolfiniun  21997  ovoliunlem3  22000  voliunlem3  22047  ioombl1  22057  mbfmax  22141  mbfpos  22143  itg1climres  22206  mbfi1fseqlem2  22208  mbfi1fseqlem6  22212  mbfi1fseq  22213  mbfmullem  22217  itg2split  22241  itg2monolem1  22242  itg2monolem3  22244  itg2mono  22245  itg2i1fseqle  22246  itg2i1fseq  22247  itg2i1fseq2  22248  itg2addlem  22250  rolle  22476  dvlip  22479  c1lip1  22483  dvcnvrelem1  22503  dvcvx  22506  ply1divex  22622  q1pval  22639  fta1glem2  22652  fta1g  22653  fta1b  22655  plydivlem3  22776  fta1lem  22788  fta1  22789  aalioulem3  22815  aalioulem4  22816  aaliou3lem2  22824  aaliou3lem8  22826  aaliou3lem9  22831  ulmdvlem1  22880  ulmdvlem3  22882  abelthlem2  22912  abelthlem7a  22917  argrege0  23083  cxplt  23162  cxplea  23164  cxple2  23165  cxplt3  23168  logbleb  23241  logblt  23242  rlimcxp  23420  scvxcvx  23432  jensenlem2  23434  ftalem3  23465  ftalem7  23469  vmalelog  23597  chtub  23604  chpchtsum  23611  bclbnd  23672  efexple  23673  bposlem5  23680  bposlem6  23681  bposlem7  23682  lgsdilem  23714  dchrisumlem3  23793  dchrmusumlema  23795  dchrmusum2  23796  dchrvmasumlem2  23800  dchrvmasumlema  23802  dchrvmasumiflem1  23803  dchrisum0flblem2  23811  dchrisum0flb  23812  dchrisum0lema  23816  dchrisum0lem1b  23817  dchrisum0lem2  23820  pntrlog2bndlem2  23880  pntibndlem2  23893  pntlemf  23907  ostth2lem1  23920  qabvle  23927  legso  24105  iscgra  24289  brbtwn2  24329  axlowdim  24385  sizeusglecusg  24607  isrusgra  25048  extwwlkfablem2  25199  isnvlem  25620  nvtri  25690  nmlnoubi  25828  nmblolbii  25831  nmblolbi  25832  blocnilem  25836  sii  25886  ubthlem2  25904  minvecolem3  25909  minvecolem5  25914  minvecolem6  25915  norm-ii  26172  norm3dif  26184  norm3adifi  26187  bcs  26215  pjnorm  26759  pjnel  26761  nmbdoplbi  27059  nmbdoplb  27060  nmcoplb  27065  lnconi  27068  nmbdfnlb  27085  nmcfnlb  27089  pjdifnormi  27202  mdslmd2i  27365  cvmd  27371  cvexch  27409  cdj1i  27468  cdj3lem1  27469  cdj3lem2b  27472  cdj3lem3b  27475  cdj3i  27476  isoun  27667  isomnd  27844  omndadd  27849  omndmul  27857  ogrpinvlt  27867  isinftm  27878  gsumle  27923  xrmulc1cn  28066  lmdvg  28089  nexple  28158  faeval  28374  brfae  28376  inelcarsg  28438  carsgsigalem  28442  carsgclctunlem2  28446  carsgclctun  28448  sconpht  28863  snmlval  28965  lediv2aALT  29232  faclim  29337  poseq  29498  sltval2  29581  sltres  29589  nodense  29614  nobndup  29625  nobnddown  29626  fvtransport  29835  idinside  29887  btwnconn1lem7  29896  btwnconn1lem11  29900  btwnconn1lem12  29901  heicant  30214  itg2addnclem  30232  itg2addnclem3  30234  itg2gt0cn  30236  ftc1anclem6  30261  ftc1anc  30264  ftc2nc  30265  dvasin  30269  areacirclem1  30273  nn0prpwlem  30306  seqpo  30406  incsequz  30407  metf1o  30414  mettrifi  30416  cntotbnd  30458  heiborlem4  30476  heiborlem6  30478  heiborlem10  30482  bfplem1  30484  bfplem2  30485  irrapxlem2  30924  irrapxlem4  30926  irrapxlem5  30927  irrapxlem6  30928  pellexlem3  30932  monotuz  31042  monotoddzzfi  31043  monotoddzz  31044  expmordi  31048  jm2.17a  31063  jm2.17b  31064  rmygeid  31067  rmydioph  31122  expdiophlem1  31129  expdiophlem2  31130  ttac  31144  fnwe2lem2  31163  cvgdvgrat  31362  monoords  31662  evthiccabs  31695  fprodle  31770  climinf  31778  climinff  31783  ioodvbdlimc1lem1  31894  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  iblspltprt  31938  itgspltprt  31944  stoweidlem3  31951  fourierdlem2  32057  fourierdlem3  32058  fourierdlem11  32066  fourierdlem12  32067  fourierdlem15  32070  fourierdlem34  32089  fourierdlem41  32096  fourierdlem48  32103  fourierdlem49  32104  fourierdlem79  32134  fourierdlem83  32138  fourierdlem89  32144  fourierdlem91  32146  fourierdlem100  32155  fourierdlem107  32162  fourierdlem109  32164  fourierdlem112  32167  etransclem31  32214  etransclem32  32215  2elfz2melfz  32655  ismgmALT  32865  iscmgmALT  32866  issgrpALT  32867  iscsgrpALT  32868  lindslinindsimp2lem5  33263  aacllem  33550  isopos  35318  oplecon3b  35338  atlatle  35458  4at2  35751  pmaple  35898  islaut  36220  lautcnvle  36226  lautco  36234  ltrncnvel  36279  cdlemeg49lebilem  36678  cdlemg17h  36807  tendoset  36898  tendotp  36900  cdlemk39s  37078  relexp01min  38237
  Copyright terms: Public domain W3C validator