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

Theorem breq12d 4217
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 4209 . 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 1652   class class class wbr 4204
This theorem is referenced by:  breq123d  4218  3brtr3d  4233  3brtr4d  4234  pocl  4502  cnvpo  5402  isoeq1  6031  isocnv  6042  isotr  6048  caovordig  6244  caovordg  6246  caovord2d  6248  caovord  6250  ofrfval  6305  ofrval  6307  ofrfval2  6315  caofref  6322  fnwelem  6453  fundmeng  7173  xpsneng  7185  xpcomeng  7192  xpdom2g  7196  map2xp  7269  mapdom3  7271  limensuc  7276  infensuc  7277  unxpdom  7308  pssnn  7319  dif1enOLD  7332  dif1en  7333  unfilem3  7365  unfi  7366  domunfican  7371  fodomfi  7377  marypha1lem  7430  wemaplem1  7507  wemaplem2  7508  wemapwe  7646  dif1card  7884  infxpenlem  7887  pwsdompw  8076  infmap2  8090  sornom  8149  isfin5  8171  isfin6  8172  domtriomlem  8314  axdc2lem  8320  axdclem2  8392  pwcfsdom  8450  cfpwsdom  8451  alephom  8452  fpwwe2lem7  8503  fpwwe2lem9  8505  pwxpndom2  8532  tskcard  8648  ordpipq  8811  adderpqlem  8823  mulerpqlem  8824  mulcanenq  8829  lterpq  8839  ltanq  8840  ltmnq  8841  ltaddnq  8843  ltrnq  8848  archnq  8849  reclem4pr  8919  ltasr  8967  sqgt0sr  8973  axpre-ltadd  9034  axpre-mulgt0  9035  ltadd1  9487  leadd2  9489  ltmul2  9853  lemul2  9855  lemul1a  9856  ltdiv1  9866  ltdiv2  9887  lediv2  9892  uzindOLD  10356  xleadd1  10826  xltadd2  10828  xsubge0  10832  xlemul1a  10859  xlemul1  10861  xlemul2  10862  xltmul2  10864  fzennn  11299  monoord  11345  monoord2  11346  ltexp2r  11428  leexp1a  11430  sqlecan  11479  bernneq  11497  faclbnd  11573  faclbnd3  11575  faclbnd4lem1  11576  faclbnd4lem2  11577  faclbnd4lem3  11578  faclbnd4lem4  11579  faclbnd6  11582  facubnd  11583  rlimcld2  12364  isercoll2  12454  climsup  12455  iseraltlem2  12468  fsumabs  12572  fsumrlim  12582  climcndslem1  12621  climcndslem2  12622  supcvg  12627  geomulcvg  12645  cvgrat  12652  ruclem2  12823  ruclem8  12828  sadcaddlem  12961  sadcadd  12962  nn0seqcvgd  13053  algcvg  13059  algcvga  13062  eucalgcvga  13069  isprm5  13104  qnumgt0  13134  pcprendvds2  13207  pcpremul  13209  pcadd2  13251  prmreclem4  13279  prmreclem5  13280  prmreclem6  13281  2expltfac  13418  xpsle  13798  mreexexlemd  13861  issubc  14027  latjlej2  14487  latmlem2  14503  sylow1lem3  15226  isslw  15234  fislw  15251  efgi  15343  lt6abl  15496  ablfac1eu  15623  isabv  15899  abvtri  15910  isucn  18300  ispsmet  18327  psmettri2  18332  ismet  18345  isxmet  18346  xmettri2  18362  imasdsf1olem  18395  imasf1oxmet  18397  blvalps  18407  blval  18408  comet  18535  stdbdxmet  18537  nrmmetd  18614  tngngp  18687  nmofval  18740  nmolb2d  18744  nmoi  18754  nmoix  18755  icopnfhmeo  18960  xrhmeo  18963  evth2  18977  pi1grplem  19066  minveclem6  19327  ovolfiniun  19389  ovoliunlem3  19392  voliunlem3  19438  ioombl1  19448  mbfmax  19533  mbfpos  19535  itg1climres  19598  mbfi1fseqlem2  19600  mbfi1fseqlem6  19604  mbfi1fseq  19605  mbfmullem  19609  itg2split  19633  itg2monolem1  19634  itg2monolem3  19636  itg2mono  19637  itg2i1fseqle  19638  itg2i1fseq  19639  itg2i1fseq2  19640  itg2addlem  19642  rolle  19866  dvlip  19869  c1lip1  19873  dvcnvrelem1  19893  dvcvx  19896  ply1divex  20051  q1pval  20068  fta1glem2  20081  fta1g  20082  fta1b  20084  plydivlem3  20204  fta1lem  20216  fta1  20217  aalioulem3  20243  aalioulem4  20244  aaliou3lem2  20252  aaliou3lem8  20254  aaliou3lem9  20259  ulmdvlem1  20308  ulmdvlem3  20310  abelthlem2  20340  abelthlem7a  20345  argrege0  20498  cxplt  20577  cxplea  20579  cxple2  20580  cxplt3  20583  rlimcxp  20804  scvxcvx  20816  jensenlem2  20818  ftalem3  20849  ftalem7  20853  vmalelog  20981  chtub  20988  chpchtsum  20995  bclbnd  21056  efexple  21057  bposlem5  21064  bposlem6  21065  bposlem7  21066  lgsdilem  21098  dchrisumlem3  21177  dchrmusumlema  21179  dchrmusum2  21180  dchrvmasumlem2  21184  dchrvmasumlema  21186  dchrvmasumiflem1  21187  dchrisum0flblem2  21195  dchrisum0flb  21196  dchrisum0lema  21200  dchrisum0lem1b  21201  dchrisum0lem2  21204  pntrlog2bndlem2  21264  pntibndlem2  21277  pntlemf  21291  ostth2lem1  21304  qabvle  21311  sizeusglecusg  21487  isnvlem  22081  nvtri  22151  nmlnoubi  22289  nmblolbii  22292  nmblolbi  22293  blocnilem  22297  sii  22347  ubthlem2  22365  minvecolem3  22370  minvecolem5  22375  minvecolem6  22376  norm-ii  22632  norm3dif  22644  norm3adifi  22647  bcs  22675  pjnorm  23218  pjnel  23220  nmbdoplbi  23519  nmbdoplb  23520  nmcoplb  23525  lnconi  23528  nmbdfnlb  23545  nmcfnlb  23549  pjdifnormi  23662  mdslmd2i  23825  cvmd  23831  cvexch  23869  cdj1i  23928  cdj3lem1  23929  cdj3lem2b  23932  cdj3lem3b  23935  cdj3i  23936  csbcnvg  24029  isoun  24081  isofld  24227  ofldadd  24230  isinftm  24243  pstmxmet  24284  xrmulc1cn  24308  lmdvg  24330  logblt  24398  faeval  24589  brfae  24591  sconpht  24908  snmlval  25010  lediv2aALT  25109  ntrivcvgtail  25220  faclim  25357  poseq  25520  sltval2  25603  sltres  25611  nodense  25636  nobndup  25647  nobnddown  25648  brbtwn2  25836  axlowdim  25892  fvtransport  25958  idinside  26010  btwnconn1lem7  26019  btwnconn1lem11  26023  btwnconn1lem12  26024  itg2addnclem  26246  itg2addnclem3  26248  itg2gt0cn  26250  ftc1anclem6  26275  ftc1anc  26278  ftc2nc  26279  dvreasin  26280  areacirclem2  26282  nn0prpwlem  26316  seqpo  26442  incsequz  26443  metf1o  26452  mettrifi  26454  cntotbnd  26496  heiborlem4  26514  heiborlem6  26516  heiborlem10  26520  bfplem1  26522  bfplem2  26523  irrapxlem2  26877  irrapxlem4  26879  irrapxlem5  26880  irrapxlem6  26881  pellexlem3  26885  monotuz  26995  monotoddzzfi  26996  monotoddzz  26997  expmordi  27001  jm2.17a  27016  jm2.17b  27017  rmygeid  27020  rmydioph  27076  expdiophlem1  27083  expdiophlem2  27084  ttac  27098  fnwe2lem2  27117  climinf  27699  climinff  27704  stoweidlem3  27719  sbcfun  27954  2elfz2melfz  28101  ltdifltdiv  28126  isopos  29915  oplecon3b  29935  atlatle  30055  4at2  30348  pmaple  30495  islaut  30817  lautcnvle  30823  lautco  30831  ltrncnvel  30876  cdlemeg49lebilem  31273  cdlemg17h  31402  tendoset  31493  tendotp  31495  cdlemk39s  31673
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205
  Copyright terms: Public domain W3C validator