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

Theorem breq12d 4293
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 4285 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 654 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362   class class class wbr 4280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281
This theorem is referenced by:  breq123d  4294  3brtr3d  4309  3brtr4d  4310  sbcbr  4333  pocl  4635  csbcnvgOLD  5011  cnvpo  5363  sbcfung  5429  isoeq1  5997  isocnv  6008  isotr  6014  caovordig  6257  caovordg  6259  caovord2d  6261  caovord  6263  ofrfval  6317  ofrval  6319  ofrfval2  6326  caofref  6335  fnwelem  6676  fundmeng  7372  xpsneng  7384  xpcomeng  7391  xpdom2g  7395  map2xp  7469  mapdom3  7471  limensuc  7476  infensuc  7477  unxpdom  7508  pssnn  7519  dif1enOLD  7532  dif1en  7533  unfilem3  7566  unfi  7567  domunfican  7572  fodomfi  7578  marypha1lem  7671  wemaplem1  7748  wemaplem2  7749  wemapwe  7916  wemapweOLD  7917  dif1card  8165  infxpenlem  8168  pwsdompw  8361  infmap2  8375  sornom  8434  isfin5  8456  isfin6  8457  domtriomlem  8599  axdc2lem  8605  axdclem2  8677  pwcfsdom  8735  cfpwsdom  8736  alephom  8737  fpwwe2lem7  8791  fpwwe2lem9  8793  pwxpndom2  8820  tskcard  8936  ordpipq  9099  adderpqlem  9111  mulerpqlem  9112  mulcanenq  9117  lterpq  9127  ltanq  9128  ltmnq  9129  ltaddnq  9131  ltrnq  9136  archnq  9137  reclem4pr  9207  ltasr  9255  sqgt0sr  9261  axpre-ltadd  9322  axpre-mulgt0  9323  ltadd1  9794  leadd2  9796  ltmul2  10168  lemul2  10170  lemul1a  10171  ltdiv1  10181  ltdiv2  10205  lediv2  10210  uzindOLD  10724  xleadd1  11206  xltadd2  11208  xsubge0  11212  xlemul1a  11239  xlemul1  11241  xlemul2  11242  xltmul2  11244  ltdifltdiv  11662  fzennn  11774  monoord  11820  monoord2  11821  ltexp2r  11904  leexp1a  11906  sqlecan  11956  bernneq  11974  faclbnd  12050  faclbnd3  12052  faclbnd4lem1  12053  faclbnd4lem2  12054  faclbnd4lem3  12055  faclbnd4lem4  12056  faclbnd6  12059  facubnd  12060  rlimcld2  13040  isercoll2  13130  climsup  13131  iseraltlem2  13144  fsumabs  13247  fsumrlim  13257  climcndslem1  13295  climcndslem2  13296  supcvg  13301  geomulcvg  13319  cvgrat  13326  ruclem2  13497  ruclem8  13502  sadcaddlem  13636  sadcadd  13637  nn0seqcvgd  13728  algcvg  13734  algcvga  13737  eucalgcvga  13744  isprm5  13781  qnumgt0  13811  pcprendvds2  13891  pcpremul  13893  pcadd2  13935  prmreclem4  13963  prmreclem5  13964  prmreclem6  13965  2expltfac  14102  xpsle  14502  mreexexlemd  14565  issubc  14731  latjlej2  15219  latmlem2  15235  sylow1lem3  16079  isslw  16087  fislw  16104  efgi  16196  lt6abl  16351  ablfac1eu  16548  isabv  16828  abvtri  16839  isucn  19695  ispsmet  19722  psmettri2  19727  ismet  19740  isxmet  19741  xmettri2  19757  imasdsf1olem  19790  imasf1oxmet  19792  blvalps  19802  blval  19803  comet  19930  stdbdxmet  19932  nrmmetd  20009  tngngp  20082  nmofval  20135  nmolb2d  20139  nmoi  20149  nmoix  20150  icopnfhmeo  20357  xrhmeo  20360  evth2  20374  pi1grplem  20463  minveclem6  20763  ovolfiniun  20826  ovoliunlem3  20829  voliunlem3  20875  ioombl1  20885  mbfmax  20969  mbfpos  20971  itg1climres  21034  mbfi1fseqlem2  21036  mbfi1fseqlem6  21040  mbfi1fseq  21041  mbfmullem  21045  itg2split  21069  itg2monolem1  21070  itg2monolem3  21072  itg2mono  21073  itg2i1fseqle  21074  itg2i1fseq  21075  itg2i1fseq2  21076  itg2addlem  21078  rolle  21304  dvlip  21307  c1lip1  21311  dvcnvrelem1  21331  dvcvx  21334  ply1divex  21493  q1pval  21510  fta1glem2  21523  fta1g  21524  fta1b  21526  plydivlem3  21646  fta1lem  21658  fta1  21659  aalioulem3  21685  aalioulem4  21686  aaliou3lem2  21694  aaliou3lem8  21696  aaliou3lem9  21701  ulmdvlem1  21750  ulmdvlem3  21752  abelthlem2  21782  abelthlem7a  21787  argrege0  21945  cxplt  22024  cxplea  22026  cxple2  22027  cxplt3  22030  rlimcxp  22252  scvxcvx  22264  jensenlem2  22266  ftalem3  22297  ftalem7  22301  vmalelog  22429  chtub  22436  chpchtsum  22443  bclbnd  22504  efexple  22505  bposlem5  22512  bposlem6  22513  bposlem7  22514  lgsdilem  22546  dchrisumlem3  22625  dchrmusumlema  22627  dchrmusum2  22628  dchrvmasumlem2  22632  dchrvmasumlema  22634  dchrvmasumiflem1  22635  dchrisum0flblem2  22643  dchrisum0flb  22644  dchrisum0lema  22648  dchrisum0lem1b  22649  dchrisum0lem2  22652  pntrlog2bndlem2  22712  pntibndlem2  22725  pntlemf  22739  ostth2lem1  22752  qabvle  22759  brbtwn2  22974  axlowdim  23030  sizeusglecusg  23217  isnvlem  23811  nvtri  23881  nmlnoubi  24019  nmblolbii  24022  nmblolbi  24023  blocnilem  24027  sii  24077  ubthlem2  24095  minvecolem3  24100  minvecolem5  24105  minvecolem6  24106  norm-ii  24363  norm3dif  24375  norm3adifi  24378  bcs  24406  pjnorm  24950  pjnel  24952  nmbdoplbi  25251  nmbdoplb  25252  nmcoplb  25257  lnconi  25260  nmbdfnlb  25277  nmcfnlb  25281  pjdifnormi  25394  mdslmd2i  25557  cvmd  25563  cvexch  25601  cdj1i  25660  cdj3lem1  25661  cdj3lem2b  25664  cdj3lem3b  25667  cdj3i  25668  isoun  25821  mul2lt0rlt0  25863  isomnd  25988  omndadd  25993  omndmul  26001  ogrpaddltbi  26006  ogrpinvlt  26011  isinftm  26022  archiabllem2b  26037  gsumle  26098  pstmxmet  26178  xrmulc1cn  26214  lmdvg  26237  nexple  26302  logblt  26319  faeval  26516  brfae  26518  sconpht  26966  snmlval  27068  lediv2aALT  27169  ntrivcvgtail  27262  faclim  27399  poseq  27561  sltval2  27644  sltres  27652  nodense  27677  nobndup  27688  nobnddown  27689  fvtransport  27910  idinside  27962  btwnconn1lem7  27971  btwnconn1lem11  27975  btwnconn1lem12  27976  heicant  28270  itg2addnclem  28287  itg2addnclem3  28289  itg2gt0cn  28291  ftc1anclem6  28316  ftc1anc  28319  ftc2nc  28320  dvasin  28324  areacirclem1  28328  nn0prpwlem  28361  seqpo  28487  incsequz  28488  metf1o  28495  mettrifi  28497  cntotbnd  28539  heiborlem4  28557  heiborlem6  28559  heiborlem10  28563  bfplem1  28565  bfplem2  28566  irrapxlem2  29009  irrapxlem4  29011  irrapxlem5  29012  irrapxlem6  29013  pellexlem3  29017  monotuz  29127  monotoddzzfi  29128  monotoddzz  29129  expmordi  29133  jm2.17a  29148  jm2.17b  29149  rmygeid  29152  rmydioph  29208  expdiophlem1  29215  expdiophlem2  29216  ttac  29230  fnwe2lem2  29249  climinf  29625  climinff  29630  stoweidlem3  29644  2elfz2melfz  30048  isrusgra  30390  extwwlkfablem2  30517  lindslinindsimp2lem5  30705  isopos  32398  oplecon3b  32418  atlatle  32538  4at2  32831  pmaple  32978  islaut  33300  lautcnvle  33306  lautco  33314  ltrncnvel  33359  cdlemeg49lebilem  33756  cdlemg17h  33885  tendoset  33976  tendotp  33978  cdlemk39s  34156
  Copyright terms: Public domain W3C validator