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

Theorem breq12d 4450
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 4442 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383   class class class wbr 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438
This theorem is referenced by:  breq123d  4451  3brtr3d  4466  3brtr4d  4467  sbcbr  4490  pocl  4797  csbcnvgALT  5177  cnvpo  5535  sbcfung  5601  isoeq1  6200  isocnv  6211  isotr  6217  caovordig  6465  caovordg  6467  caovord2d  6469  caovord  6471  ofrfval  6533  ofrval  6535  ofrfval2  6542  caofref  6551  fnwelem  6900  fundmeng  7592  xpsneng  7604  xpcomeng  7611  xpdom2g  7615  map2xp  7689  mapdom3  7691  limensuc  7696  infensuc  7697  unxpdom  7729  pssnn  7740  dif1enOLD  7754  dif1en  7755  unfilem3  7788  unfi  7789  domunfican  7795  fodomfi  7801  marypha1lem  7895  wemaplem1  7974  wemaplem2  7975  wemapwe  8142  wemapweOLD  8143  dif1card  8391  infxpenlem  8394  pwsdompw  8587  infmap2  8601  sornom  8660  isfin5  8682  isfin6  8683  domtriomlem  8825  axdc2lem  8831  axdclem2  8903  pwcfsdom  8961  cfpwsdom  8962  alephom  8963  fpwwe2lem7  9017  fpwwe2lem9  9019  pwxpndom2  9046  tskcard  9162  ordpipq  9323  adderpqlem  9335  mulerpqlem  9336  mulcanenq  9341  lterpq  9351  ltanq  9352  ltmnq  9353  ltaddnq  9355  ltrnq  9360  archnq  9361  reclem4pr  9431  ltasr  9480  sqgt0sr  9486  axpre-ltadd  9547  axpre-mulgt0  9548  ltadd1  10026  leadd2  10028  ltmul2  10400  lemul2  10402  lemul1a  10403  ltdiv1  10413  ltdiv2  10437  lediv2  10442  uzindOLD  10964  xleadd1  11458  xltadd2  11460  xsubge0  11464  xlemul1a  11491  xlemul1  11493  xlemul2  11494  xltmul2  11496  ltdifltdiv  11948  fzennn  12060  monoord  12119  monoord2  12120  ltexp2r  12204  leexp1a  12206  sqlecan  12256  bernneq  12274  faclbnd  12350  faclbnd3  12352  faclbnd4lem1  12353  faclbnd4lem2  12354  faclbnd4lem3  12355  faclbnd4lem4  12356  faclbnd6  12359  facubnd  12360  rlimcld2  13383  isercoll2  13473  climsup  13474  iseraltlem2  13487  fsumabs  13597  fsumrlim  13607  climcndslem1  13643  climcndslem2  13644  supcvg  13649  geomulcvg  13667  cvgrat  13674  ntrivcvgtail  13691  ruclem2  13947  ruclem8  13952  sadcaddlem  14089  sadcadd  14090  nn0seqcvgd  14181  algcvg  14187  algcvga  14190  eucalgcvga  14197  isprm5  14235  qnumgt0  14265  pcprendvds2  14347  pcpremul  14349  pcadd2  14391  prmreclem4  14419  prmreclem5  14420  prmreclem6  14421  2expltfac  14559  xpsle  14960  mreexexlemd  15023  issubc  15186  latjlej2  15675  latmlem2  15691  sylow1lem3  16599  isslw  16607  fislw  16624  efgi  16716  lt6abl  16876  ablfac1eu  17103  isabv  17447  abvtri  17458  cayleyhamilton1  19371  isucn  20759  ispsmet  20786  psmettri2  20791  ismet  20804  isxmet  20805  xmettri2  20821  imasdsf1olem  20854  imasf1oxmet  20856  blvalps  20866  blval  20867  comet  20994  stdbdxmet  20996  nrmmetd  21073  tngngp  21146  nmofval  21199  nmolb2d  21203  nmoi  21213  nmoix  21214  icopnfhmeo  21421  xrhmeo  21424  evth2  21438  pi1grplem  21527  minveclem6  21827  ovolfiniun  21890  ovoliunlem3  21893  voliunlem3  21940  ioombl1  21950  mbfmax  22034  mbfpos  22036  itg1climres  22099  mbfi1fseqlem2  22101  mbfi1fseqlem6  22105  mbfi1fseq  22106  mbfmullem  22110  itg2split  22134  itg2monolem1  22135  itg2monolem3  22137  itg2mono  22138  itg2i1fseqle  22139  itg2i1fseq  22140  itg2i1fseq2  22141  itg2addlem  22143  rolle  22369  dvlip  22372  c1lip1  22376  dvcnvrelem1  22396  dvcvx  22399  ply1divex  22515  q1pval  22532  fta1glem2  22545  fta1g  22546  fta1b  22548  plydivlem3  22669  fta1lem  22681  fta1  22682  aalioulem3  22708  aalioulem4  22709  aaliou3lem2  22717  aaliou3lem8  22719  aaliou3lem9  22724  ulmdvlem1  22773  ulmdvlem3  22775  abelthlem2  22805  abelthlem7a  22810  argrege0  22974  cxplt  23053  cxplea  23055  cxple2  23056  cxplt3  23059  rlimcxp  23281  scvxcvx  23293  jensenlem2  23295  ftalem3  23326  ftalem7  23330  vmalelog  23458  chtub  23465  chpchtsum  23472  bclbnd  23533  efexple  23534  bposlem5  23541  bposlem6  23542  bposlem7  23543  lgsdilem  23575  dchrisumlem3  23654  dchrmusumlema  23656  dchrmusum2  23657  dchrvmasumlem2  23661  dchrvmasumlema  23663  dchrvmasumiflem1  23664  dchrisum0flblem2  23672  dchrisum0flb  23673  dchrisum0lema  23677  dchrisum0lem1b  23678  dchrisum0lem2  23681  pntrlog2bndlem2  23741  pntibndlem2  23754  pntlemf  23768  ostth2lem1  23781  qabvle  23788  legso  23963  iscgra  24147  brbtwn2  24186  axlowdim  24242  sizeusglecusg  24464  isrusgra  24905  extwwlkfablem2  25056  isnvlem  25481  nvtri  25551  nmlnoubi  25689  nmblolbii  25692  nmblolbi  25693  blocnilem  25697  sii  25747  ubthlem2  25765  minvecolem3  25770  minvecolem5  25775  minvecolem6  25776  norm-ii  26033  norm3dif  26045  norm3adifi  26048  bcs  26076  pjnorm  26620  pjnel  26622  nmbdoplbi  26921  nmbdoplb  26922  nmcoplb  26927  lnconi  26930  nmbdfnlb  26947  nmcfnlb  26951  pjdifnormi  27064  mdslmd2i  27227  cvmd  27233  cvexch  27271  cdj1i  27330  cdj3lem1  27331  cdj3lem2b  27334  cdj3lem3b  27337  cdj3i  27338  isoun  27498  isomnd  27669  omndadd  27674  omndmul  27682  ogrpinvlt  27692  isinftm  27703  gsumle  27748  xrmulc1cn  27890  lmdvg  27913  nexple  27983  logblt  28000  faeval  28196  brfae  28198  sconpht  28652  snmlval  28754  lediv2aALT  29021  faclim  29147  poseq  29309  sltval2  29392  sltres  29400  nodense  29425  nobndup  29436  nobnddown  29437  fvtransport  29658  idinside  29710  btwnconn1lem7  29719  btwnconn1lem11  29723  btwnconn1lem12  29724  heicant  30025  itg2addnclem  30042  itg2addnclem3  30044  itg2gt0cn  30046  ftc1anclem6  30071  ftc1anc  30074  ftc2nc  30075  dvasin  30079  areacirclem1  30083  nn0prpwlem  30116  seqpo  30216  incsequz  30217  metf1o  30224  mettrifi  30226  cntotbnd  30268  heiborlem4  30286  heiborlem6  30288  heiborlem10  30292  bfplem1  30294  bfplem2  30295  irrapxlem2  30735  irrapxlem4  30737  irrapxlem5  30738  irrapxlem6  30739  pellexlem3  30743  monotuz  30853  monotoddzzfi  30854  monotoddzz  30855  expmordi  30859  jm2.17a  30874  jm2.17b  30875  rmygeid  30878  rmydioph  30932  expdiophlem1  30939  expdiophlem2  30940  ttac  30954  fnwe2lem2  30973  cvgdvgrat  31170  monoords  31450  evthiccabs  31483  fprodle  31558  climinf  31566  climinff  31571  ioodvbdlimc1lem1  31682  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  iblspltprt  31726  itgspltprt  31732  stoweidlem3  31739  fourierdlem2  31845  fourierdlem3  31846  fourierdlem11  31854  fourierdlem12  31855  fourierdlem15  31858  fourierdlem34  31877  fourierdlem41  31884  fourierdlem48  31891  fourierdlem49  31892  fourierdlem79  31922  fourierdlem83  31926  fourierdlem89  31932  fourierdlem91  31934  fourierdlem100  31943  fourierdlem107  31950  fourierdlem109  31952  fourierdlem112  31955  etransclem31  32002  etransclem32  32003  etransclem38  32009  2elfz2melfz  32288  ismgmALT  32500  iscmgmALT  32501  issgrpALT  32502  iscsgrpALT  32503  lindslinindsimp2lem5  32933  isopos  34780  oplecon3b  34800  atlatle  34920  4at2  35213  pmaple  35360  islaut  35682  lautcnvle  35688  lautco  35696  ltrncnvel  35741  cdlemeg49lebilem  36140  cdlemg17h  36269  tendoset  36360  tendotp  36362  cdlemk39s  36540
  Copyright terms: Public domain W3C validator