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

Theorem breq12d 4414
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 4406 . 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 1370   class class class wbr 4401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-br 4402
This theorem is referenced by:  breq123d  4415  3brtr3d  4430  3brtr4d  4431  sbcbr  4454  pocl  4757  csbcnvgALT  5133  cnvpo  5484  sbcfung  5550  isoeq1  6120  isocnv  6131  isotr  6137  caovordig  6379  caovordg  6381  caovord2d  6383  caovord  6385  ofrfval  6439  ofrval  6441  ofrfval2  6448  caofref  6457  fnwelem  6798  fundmeng  7495  xpsneng  7507  xpcomeng  7514  xpdom2g  7518  map2xp  7592  mapdom3  7594  limensuc  7599  infensuc  7600  unxpdom  7632  pssnn  7643  dif1enOLD  7656  dif1en  7657  unfilem3  7690  unfi  7691  domunfican  7696  fodomfi  7702  marypha1lem  7795  wemaplem1  7872  wemaplem2  7873  wemapwe  8040  wemapweOLD  8041  dif1card  8289  infxpenlem  8292  pwsdompw  8485  infmap2  8499  sornom  8558  isfin5  8580  isfin6  8581  domtriomlem  8723  axdc2lem  8729  axdclem2  8801  pwcfsdom  8859  cfpwsdom  8860  alephom  8861  fpwwe2lem7  8915  fpwwe2lem9  8917  pwxpndom2  8944  tskcard  9060  ordpipq  9223  adderpqlem  9235  mulerpqlem  9236  mulcanenq  9241  lterpq  9251  ltanq  9252  ltmnq  9253  ltaddnq  9255  ltrnq  9260  archnq  9261  reclem4pr  9331  ltasr  9379  sqgt0sr  9385  axpre-ltadd  9446  axpre-mulgt0  9447  ltadd1  9918  leadd2  9920  ltmul2  10292  lemul2  10294  lemul1a  10295  ltdiv1  10305  ltdiv2  10329  lediv2  10334  uzindOLD  10848  xleadd1  11330  xltadd2  11332  xsubge0  11336  xlemul1a  11363  xlemul1  11365  xlemul2  11366  xltmul2  11368  ltdifltdiv  11796  fzennn  11908  monoord  11954  monoord2  11955  ltexp2r  12038  leexp1a  12040  sqlecan  12090  bernneq  12108  faclbnd  12184  faclbnd3  12186  faclbnd4lem1  12187  faclbnd4lem2  12188  faclbnd4lem3  12189  faclbnd4lem4  12190  faclbnd6  12193  facubnd  12194  rlimcld2  13175  isercoll2  13265  climsup  13266  iseraltlem2  13279  fsumabs  13383  fsumrlim  13393  climcndslem1  13431  climcndslem2  13432  supcvg  13437  geomulcvg  13455  cvgrat  13462  ruclem2  13633  ruclem8  13638  sadcaddlem  13772  sadcadd  13773  nn0seqcvgd  13864  algcvg  13870  algcvga  13873  eucalgcvga  13880  isprm5  13917  qnumgt0  13947  pcprendvds2  14027  pcpremul  14029  pcadd2  14071  prmreclem4  14099  prmreclem5  14100  prmreclem6  14101  2expltfac  14238  xpsle  14639  mreexexlemd  14702  issubc  14868  latjlej2  15356  latmlem2  15372  sylow1lem3  16221  isslw  16229  fislw  16246  efgi  16338  lt6abl  16493  ablfac1eu  16697  isabv  17028  abvtri  17039  isucn  19986  ispsmet  20013  psmettri2  20018  ismet  20031  isxmet  20032  xmettri2  20048  imasdsf1olem  20081  imasf1oxmet  20083  blvalps  20093  blval  20094  comet  20221  stdbdxmet  20223  nrmmetd  20300  tngngp  20373  nmofval  20426  nmolb2d  20430  nmoi  20440  nmoix  20441  icopnfhmeo  20648  xrhmeo  20651  evth2  20665  pi1grplem  20754  minveclem6  21054  ovolfiniun  21117  ovoliunlem3  21120  voliunlem3  21167  ioombl1  21177  mbfmax  21261  mbfpos  21263  itg1climres  21326  mbfi1fseqlem2  21328  mbfi1fseqlem6  21332  mbfi1fseq  21333  mbfmullem  21337  itg2split  21361  itg2monolem1  21362  itg2monolem3  21364  itg2mono  21365  itg2i1fseqle  21366  itg2i1fseq  21367  itg2i1fseq2  21368  itg2addlem  21370  rolle  21596  dvlip  21599  c1lip1  21603  dvcnvrelem1  21623  dvcvx  21626  ply1divex  21742  q1pval  21759  fta1glem2  21772  fta1g  21773  fta1b  21775  plydivlem3  21895  fta1lem  21907  fta1  21908  aalioulem3  21934  aalioulem4  21935  aaliou3lem2  21943  aaliou3lem8  21945  aaliou3lem9  21950  ulmdvlem1  21999  ulmdvlem3  22001  abelthlem2  22031  abelthlem7a  22036  argrege0  22194  cxplt  22273  cxplea  22275  cxple2  22276  cxplt3  22279  rlimcxp  22501  scvxcvx  22513  jensenlem2  22515  ftalem3  22546  ftalem7  22550  vmalelog  22678  chtub  22685  chpchtsum  22692  bclbnd  22753  efexple  22754  bposlem5  22761  bposlem6  22762  bposlem7  22763  lgsdilem  22795  dchrisumlem3  22874  dchrmusumlema  22876  dchrmusum2  22877  dchrvmasumlem2  22881  dchrvmasumlema  22883  dchrvmasumiflem1  22884  dchrisum0flblem2  22892  dchrisum0flb  22893  dchrisum0lema  22897  dchrisum0lem1b  22898  dchrisum0lem2  22901  pntrlog2bndlem2  22961  pntibndlem2  22974  pntlemf  22988  ostth2lem1  23001  qabvle  23008  brbtwn2  23304  axlowdim  23360  sizeusglecusg  23547  isnvlem  24141  nvtri  24211  nmlnoubi  24349  nmblolbii  24352  nmblolbi  24353  blocnilem  24357  sii  24407  ubthlem2  24425  minvecolem3  24430  minvecolem5  24435  minvecolem6  24436  norm-ii  24693  norm3dif  24705  norm3adifi  24708  bcs  24736  pjnorm  25280  pjnel  25282  nmbdoplbi  25581  nmbdoplb  25582  nmcoplb  25587  lnconi  25590  nmbdfnlb  25607  nmcfnlb  25611  pjdifnormi  25724  mdslmd2i  25887  cvmd  25893  cvexch  25931  cdj1i  25990  cdj3lem1  25991  cdj3lem2b  25994  cdj3lem3b  25997  cdj3i  25998  isoun  26149  mul2lt0rlt0  26190  isomnd  26310  omndadd  26315  omndmul  26323  ogrpaddltbi  26328  ogrpinvlt  26333  isinftm  26344  archiabllem2b  26359  gsumle  26392  pstmxmet  26470  xrmulc1cn  26506  lmdvg  26529  nexple  26594  logblt  26611  faeval  26807  brfae  26809  sconpht  27263  snmlval  27365  lediv2aALT  27467  ntrivcvgtail  27560  faclim  27697  poseq  27859  sltval2  27942  sltres  27950  nodense  27975  nobndup  27986  nobnddown  27987  fvtransport  28208  idinside  28260  btwnconn1lem7  28269  btwnconn1lem11  28273  btwnconn1lem12  28274  heicant  28575  itg2addnclem  28592  itg2addnclem3  28594  itg2gt0cn  28596  ftc1anclem6  28621  ftc1anc  28624  ftc2nc  28625  dvasin  28629  areacirclem1  28633  nn0prpwlem  28666  seqpo  28792  incsequz  28793  metf1o  28800  mettrifi  28802  cntotbnd  28844  heiborlem4  28862  heiborlem6  28864  heiborlem10  28868  bfplem1  28870  bfplem2  28871  irrapxlem2  29313  irrapxlem4  29315  irrapxlem5  29316  irrapxlem6  29317  pellexlem3  29321  monotuz  29431  monotoddzzfi  29432  monotoddzz  29433  expmordi  29437  jm2.17a  29452  jm2.17b  29453  rmygeid  29456  rmydioph  29512  expdiophlem1  29519  expdiophlem2  29520  ttac  29534  fnwe2lem2  29553  climinf  29928  climinff  29933  stoweidlem3  29947  2elfz2melfz  30351  isrusgra  30693  extwwlkfablem2  30820  lindslinindsimp2lem5  31129  cayleyhamilton1  31380  isopos  33164  oplecon3b  33184  atlatle  33304  4at2  33597  pmaple  33744  islaut  34066  lautcnvle  34072  lautco  34080  ltrncnvel  34125  cdlemeg49lebilem  34522  cdlemg17h  34651  tendoset  34742  tendotp  34744  cdlemk39s  34922
  Copyright terms: Public domain W3C validator