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

Theorem breq12d 4228
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 4220 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 644 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653   class class class wbr 4215
This theorem is referenced by:  breq123d  4229  3brtr3d  4244  3brtr4d  4245  pocl  4513  cnvpo  5413  isoeq1  6042  isocnv  6053  isotr  6059  caovordig  6255  caovordg  6257  caovord2d  6259  caovord  6261  ofrfval  6316  ofrval  6318  ofrfval2  6326  caofref  6333  fnwelem  6464  fundmeng  7184  xpsneng  7196  xpcomeng  7203  xpdom2g  7207  map2xp  7280  mapdom3  7282  limensuc  7287  infensuc  7288  unxpdom  7319  pssnn  7330  dif1enOLD  7343  dif1en  7344  unfilem3  7376  unfi  7377  domunfican  7382  fodomfi  7388  marypha1lem  7441  wemaplem1  7518  wemaplem2  7519  wemapwe  7657  dif1card  7897  infxpenlem  7900  pwsdompw  8089  infmap2  8103  sornom  8162  isfin5  8184  isfin6  8185  domtriomlem  8327  axdc2lem  8333  axdclem2  8405  pwcfsdom  8463  cfpwsdom  8464  alephom  8465  fpwwe2lem7  8516  fpwwe2lem9  8518  pwxpndom2  8545  tskcard  8661  ordpipq  8824  adderpqlem  8836  mulerpqlem  8837  mulcanenq  8842  lterpq  8852  ltanq  8853  ltmnq  8854  ltaddnq  8856  ltrnq  8861  archnq  8862  reclem4pr  8932  ltasr  8980  sqgt0sr  8986  axpre-ltadd  9047  axpre-mulgt0  9048  ltadd1  9500  leadd2  9502  ltmul2  9866  lemul2  9868  lemul1a  9869  ltdiv1  9879  ltdiv2  9900  lediv2  9905  uzindOLD  10369  xleadd1  10839  xltadd2  10841  xsubge0  10845  xlemul1a  10872  xlemul1  10874  xlemul2  10875  xltmul2  10877  fzennn  11312  monoord  11358  monoord2  11359  ltexp2r  11441  leexp1a  11443  sqlecan  11492  bernneq  11510  faclbnd  11586  faclbnd3  11588  faclbnd4lem1  11589  faclbnd4lem2  11590  faclbnd4lem3  11591  faclbnd4lem4  11592  faclbnd6  11595  facubnd  11596  rlimcld2  12377  isercoll2  12467  climsup  12468  iseraltlem2  12481  fsumabs  12585  fsumrlim  12595  climcndslem1  12634  climcndslem2  12635  supcvg  12640  geomulcvg  12658  cvgrat  12665  ruclem2  12836  ruclem8  12841  sadcaddlem  12974  sadcadd  12975  nn0seqcvgd  13066  algcvg  13072  algcvga  13075  eucalgcvga  13082  isprm5  13117  qnumgt0  13147  pcprendvds2  13220  pcpremul  13222  pcadd2  13264  prmreclem4  13292  prmreclem5  13293  prmreclem6  13294  2expltfac  13431  xpsle  13811  mreexexlemd  13874  issubc  14040  latjlej2  14500  latmlem2  14516  sylow1lem3  15239  isslw  15247  fislw  15264  efgi  15356  lt6abl  15509  ablfac1eu  15636  isabv  15912  abvtri  15923  isucn  18313  ispsmet  18340  psmettri2  18345  ismet  18358  isxmet  18359  xmettri2  18375  imasdsf1olem  18408  imasf1oxmet  18410  blvalps  18420  blval  18421  comet  18548  stdbdxmet  18550  nrmmetd  18627  tngngp  18700  nmofval  18753  nmolb2d  18757  nmoi  18767  nmoix  18768  icopnfhmeo  18973  xrhmeo  18976  evth2  18990  pi1grplem  19079  minveclem6  19340  ovolfiniun  19402  ovoliunlem3  19405  voliunlem3  19451  ioombl1  19461  mbfmax  19544  mbfpos  19546  itg1climres  19609  mbfi1fseqlem2  19611  mbfi1fseqlem6  19615  mbfi1fseq  19616  mbfmullem  19620  itg2split  19644  itg2monolem1  19645  itg2monolem3  19647  itg2mono  19648  itg2i1fseqle  19649  itg2i1fseq  19650  itg2i1fseq2  19651  itg2addlem  19653  rolle  19879  dvlip  19882  c1lip1  19886  dvcnvrelem1  19906  dvcvx  19909  ply1divex  20064  q1pval  20081  fta1glem2  20094  fta1g  20095  fta1b  20097  plydivlem3  20217  fta1lem  20229  fta1  20230  aalioulem3  20256  aalioulem4  20257  aaliou3lem2  20265  aaliou3lem8  20267  aaliou3lem9  20272  ulmdvlem1  20321  ulmdvlem3  20323  abelthlem2  20353  abelthlem7a  20358  argrege0  20511  cxplt  20590  cxplea  20592  cxple2  20593  cxplt3  20596  rlimcxp  20817  scvxcvx  20829  jensenlem2  20831  ftalem3  20862  ftalem7  20866  vmalelog  20994  chtub  21001  chpchtsum  21008  bclbnd  21069  efexple  21070  bposlem5  21077  bposlem6  21078  bposlem7  21079  lgsdilem  21111  dchrisumlem3  21190  dchrmusumlema  21192  dchrmusum2  21193  dchrvmasumlem2  21197  dchrvmasumlema  21199  dchrvmasumiflem1  21200  dchrisum0flblem2  21208  dchrisum0flb  21209  dchrisum0lema  21213  dchrisum0lem1b  21214  dchrisum0lem2  21217  pntrlog2bndlem2  21277  pntibndlem2  21290  pntlemf  21304  ostth2lem1  21317  qabvle  21324  sizeusglecusg  21500  isnvlem  22094  nvtri  22164  nmlnoubi  22302  nmblolbii  22305  nmblolbi  22306  blocnilem  22310  sii  22360  ubthlem2  22378  minvecolem3  22383  minvecolem5  22388  minvecolem6  22389  norm-ii  22645  norm3dif  22657  norm3adifi  22660  bcs  22688  pjnorm  23231  pjnel  23233  nmbdoplbi  23532  nmbdoplb  23533  nmcoplb  23538  lnconi  23541  nmbdfnlb  23558  nmcfnlb  23562  pjdifnormi  23675  mdslmd2i  23838  cvmd  23844  cvexch  23882  cdj1i  23941  cdj3lem1  23942  cdj3lem2b  23945  cdj3lem3b  23948  cdj3i  23949  csbcnvg  24042  isoun  24094  isofld  24240  ofldadd  24243  isinftm  24256  pstmxmet  24297  xrmulc1cn  24321  lmdvg  24343  logblt  24411  faeval  24602  brfae  24604  sconpht  24921  snmlval  25023  lediv2aALT  25122  ntrivcvgtail  25233  faclim  25370  poseq  25533  sltval2  25616  sltres  25624  nodense  25649  nobndup  25660  nobnddown  25661  brbtwn2  25849  axlowdim  25905  fvtransport  25971  idinside  26023  btwnconn1lem7  26032  btwnconn1lem11  26036  btwnconn1lem12  26037  heicant  26253  itg2addnclem  26270  itg2addnclem3  26272  itg2gt0cn  26274  ftc1anclem6  26299  ftc1anc  26302  ftc2nc  26303  dvreasin  26304  areacirclem1  26306  nn0prpwlem  26339  seqpo  26465  incsequz  26466  metf1o  26475  mettrifi  26477  cntotbnd  26519  heiborlem4  26537  heiborlem6  26539  heiborlem10  26543  bfplem1  26545  bfplem2  26546  irrapxlem2  26900  irrapxlem4  26902  irrapxlem5  26903  irrapxlem6  26904  pellexlem3  26908  monotuz  27018  monotoddzzfi  27019  monotoddzz  27020  expmordi  27024  jm2.17a  27039  jm2.17b  27040  rmygeid  27043  rmydioph  27099  expdiophlem1  27106  expdiophlem2  27107  ttac  27121  fnwe2lem2  27140  climinf  27722  climinff  27727  stoweidlem3  27742  sbcfun  27977  2elfz2melfz  28140  ltdifltdiv  28171  isrusgra  28442  isopos  30052  oplecon3b  30072  atlatle  30192  4at2  30485  pmaple  30632  islaut  30954  lautcnvle  30960  lautco  30968  ltrncnvel  31013  cdlemeg49lebilem  31410  cdlemg17h  31539  tendoset  31630  tendotp  31632  cdlemk39s  31810
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216
  Copyright terms: Public domain W3C validator