Theorem breq12d 5083

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	⊢ (𝜑 → 𝐴 = 𝐵)
breq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
breq12d	⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Proof of Theorem breq12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		breq12 5075	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2anc 583	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  breq123d  5084  3brtr3d  5101  3brtr4d  5102  sbcbr  5125  pocl  5501  poclOLD  5502  csbcnvgALT  5782  cnvpo  6179  sbcfung  6442  isoeq1  7168  isocnv  7181  isotr  7187  caovordig  7455  caovordg  7457  caovord2d  7459  caovord  7461  ofrfvalg  7519  ofrval  7523  ofrfval2  7532  caofref  7540  fnwelem  7943  fundmeng  8776  enrefnn  8791  xpsneng  8797  xpcomeng  8804  xpdom2g  8808  limensuc  8890  infensuc  8891  pssnn  8913  unxpdom  8959  pssnnOLD  8969  dif1enALT  8980  unfilem3  9010  unfiOLD  9011  domunfican  9017  fodomfi  9022  marypha1lem  9122  infsupprpr  9193  wemaplem1  9235  wemaplem2  9236  wemapwe  9385  dif1card  9697  infxpenlem  9700  nnadju  9884  pwsdompw  9891  infmap2  9905  sornom  9964  isfin5  9986  isfin6  9987  domtriomlem  10129  axdc2lem  10135  axdclem2  10207  pwcfsdom  10270  cfpwsdom  10271  alephom  10272  fpwwe2lem6  10323  fpwwe2lem8  10325  tskcard  10468  ordpipq  10629  adderpqlem  10641  mulerpqlem  10642  mulcanenq  10647  lterpq  10657  ltanq  10658  ltmnq  10659  ltaddnq  10661  ltrnq  10666  archnq  10667  reclem4pr  10737  ltasr  10787  sqgt0sr  10793  axpre-ltadd  10854  axpre-mulgt0  10855  ltadd1  11372  leadd2  11374  ltmul2  11756  lemul2  11758  lemul1a  11759  ltdiv1  11769  ltdiv2  11791  lediv2  11795  div4p1lem1div2  12158  nn0ledivnn  12772  xleadd1  12918  xltadd2  12920  xsubge0  12924  xlemul1a  12951  xlemul1  12953  xlemul2  12954  xltmul2  12956  ltdifltdiv  13482  fzennn  13616  monoord  13681  monoord2  13682  expmordi  13813  ltexp2r  13819  leexp1a  13821  sqlecan  13853  bernneq  13872  faclbnd  13932  faclbnd3  13934  faclbnd4lem1  13935  faclbnd4lem2  13936  faclbnd4lem3  13937  faclbnd4lem4  13938  faclbnd6  13941  facubnd  13942  rlimcld2  15215  isercoll2  15308  climsup  15309  iseraltlem2  15322  fsumabs  15441  fsumrlim  15451  climcndslem1  15489  climcndslem2  15490  supcvg  15496  geomulcvg  15516  cvgrat  15523  ntrivcvgtail  15540  ruclem2  15869  ruclem8  15874  addmodlteqALT  15962  fproddvdsd  15972  sadcaddlem  16092  sadcadd  16093  nn0seqcvgd  16203  algcvg  16209  algcvga  16212  eucalgcvga  16219  isprm5  16340  qnumgt0  16382  pcprendvds2  16470  pcpremul  16472  pcadd2  16519  prmreclem4  16548  prmreclem5  16549  prmreclem6  16550  2expltfac  16722  xpsle  17207  mreexexlemd  17270  issubc  17466  latjlej2  18087  latmlem2  18103  sylow1lem3  19120  isslw  19128  fislw  19145  efgi  19240  lt6abl  19411  ablfac1eu  19591  isabv  19994  abvtri  20005  cayleyhamilton1  21949  isucn  23338  ispsmet  23365  psmettri2  23370  ismet  23384  isxmet  23385  xmettri2  23401  imasdsf1olem  23434  imasf1oxmet  23436  blvalps  23446  blval  23447  comet  23575  stdbdxmet  23577  nrmmetd  23636  tngngp  23724  tngngp3  23726  nmofval  23784  nmolb2d  23788  nmoi  23798  nmoix  23799  icopnfhmeo  24012  xrhmeo  24015  evth2  24029  pi1grplem  24118  minveclem6  24503  ovolfiniun  24570  ovoliunlem3  24573  voliunlem3  24621  ioombl1  24631  mbfmax  24718  mbfpos  24720  itg1climres  24784  mbfi1fseqlem2  24786  mbfi1fseqlem6  24790  mbfi1fseq  24791  mbfmullem  24795  itg2split  24819  itg2monolem1  24820  itg2monolem3  24822  itg2mono  24823  itg2i1fseqle  24824  itg2i1fseq  24825  itg2i1fseq2  24826  itg2addlem  24828  rolle  25059  dvlip  25062  c1lip1  25066  dvcnvrelem1  25086  dvcvx  25089  ply1divex  25206  q1pval  25223  fta1glem2  25236  fta1g  25237  fta1b  25239  plydivlem3  25360  fta1lem  25372  fta1  25373  aalioulem3  25399  aalioulem4  25400  aaliou3lem2  25408  aaliou3lem8  25410  aaliou3lem9  25415  ulmdvlem1  25464  ulmdvlem3  25466  abelthlem2  25496  abelthlem7a  25501  argrege0  25671  cxplt  25754  cxplea  25756  cxple2  25757  cxplt3  25760  logbleb  25838  logblt  25839  rlimcxp  26028  scvxcvx  26040  jensenlem2  26042  ftalem3  26129  ftalem7  26133  vmalelog  26258  chtub  26265  chpchtsum  26272  bclbnd  26333  efexple  26334  bposlem5  26341  bposlem6  26342  bposlem7  26343  lgsdilem  26377  2lgslem1a2  26443  2sqreuop  26515  2sqreuopnn  26516  2sqreuoplt  26517  2sqreuopltb  26518  2sqreuopnnlt  26519  2sqreuopnnltb  26520  dchrisumlem3  26544  dchrmusumlema  26546  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumlema  26553  dchrvmasumiflem1  26554  dchrisum0flblem2  26562  dchrisum0flb  26563  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem2  26571  pntrlog2bndlem2  26631  pntibndlem2  26644  pntlemf  26658  ostth2lem1  26671  qabvle  26678  legso  26864  iscgra  27074  isleag  27112  iseqlg  27132  brbtwn2  27176  axlowdim  27232  ewlksfval  27871  isnvlem  28873  nvtri  28933  nmlnoubi  29059  nmblolbii  29062  nmblolbi  29063  blocnilem  29067  sii  29117  ubthlem2  29134  minvecolem3  29139  minvecolem5  29144  minvecolem6  29145  norm-ii  29401  norm3dif  29413  norm3adifi  29416  bcs  29444  pjnorm  29987  pjnel  29989  nmbdoplbi  30287  nmbdoplb  30288  nmcoplb  30293  lnconi  30296  nmbdfnlb  30313  nmcfnlb  30317  pjdifnormi  30430  mdslmd2i  30593  cvmd  30599  cvexch  30637  cdj1i  30696  cdj3lem1  30697  cdj3lem2b  30700  cdj3lem3b  30703  cdj3i  30704  isoun  30936  ismnt  31163  mgcmntco  31174  dfmgc2lem  31175  dfmgc2  31176  mgcf1o  31183  isomnd  31229  omndadd  31234  omndmul  31242  ogrpinvlt  31251  gsumle  31252  isinftm  31337  xrmulc1cn  31782  lmdvg  31805  nexple  31877  faeval  32114  brfae  32116  inelcarsg  32178  carsgsigalem  32182  carsgclctunlem2  32186  carsgclctun  32188  hgt750lemc  32527  hgt750lemd  32528  hgt749d  32529  sconnpht  33091  snmlval  33193  satfv1lem  33224  satfv1  33225  satfv0fun  33233  satfv0fvfmla0  33275  lediv2aALT  33535  faclim  33618  ssttrcl  33701  ttrcltr  33702  ttrclss  33706  dmttrcl  33707  rnttrcl  33708  ttrclselem2  33712  poseq  33729  sltval2  33786  sltres  33792  nolesgn2o  33801  nogesgn1o  33803  nodense  33822  nolt02o  33825  nogt01o  33826  noresle  33827  nosupbnd2lem1  33845  nosupbnd2  33846  noinfbnd2lem1  33860  noinfbnd2  33861  fvtransport  34261  idinside  34313  btwnconn1lem7  34322  btwnconn1lem11  34326  btwnconn1lem12  34327  nn0prpwlem  34438  bj-opabco  35286  poimirlem29  35733  heicant  35739  itg2addnclem  35755  itg2addnclem3  35757  itg2gt0cn  35759  ftc1anclem6  35782  ftc1anc  35785  ftc2nc  35786  dvasin  35788  areacirclem1  35792  seqpo  35832  incsequz  35833  metf1o  35840  mettrifi  35842  cntotbnd  35881  heiborlem4  35899  heiborlem6  35901  heiborlem10  35905  bfplem1  35907  bfplem2  35908  isopos  37121  oplecon3b  37141  atlatle  37261  4at2  37555  pmaple  37702  islaut  38024  lautcnvle  38030  lautco  38038  ltrncnvel  38083  cdlemeg49lebilem  38480  cdlemg17h  38609  tendoset  38700  tendotp  38702  cdlemk39s  38880  lcmineqlem23  39987  lcmineqlem  39988  intlewftc  39997  aks4d1p1p4  40007  dvle2  40008  aks4d1p8d2  40021  aks4d1p9  40024  aks4d1  40025  2ap1caineq  40029  sticksstones1  40030  sticksstones2  40031  sticksstones3  40032  sticksstones8  40037  sticksstones10  40039  sticksstones11  40040  sticksstones12a  40041  sticksstones15  40045  factwoffsmonot  40091  brif12  40126  dvdsexpnn0  40262  dvdsexpb  40263  reltsub1  40290  irrapxlem2  40561  irrapxlem4  40563  irrapxlem5  40564  irrapxlem6  40565  pellexlem3  40569  monotuz  40679  monotoddzzfi  40680  monotoddzz  40681  jm2.17a  40698  jm2.17b  40699  rmygeid  40702  rmydioph  40752  expdiophlem1  40759  expdiophlem2  40760  ttac  40774  fnwe2lem2  40792  relexp01min  41210  cvgdvgrat  41820  monoords  42726  supxrgelem  42766  supxrge  42767  abslt2sqd  42789  ltmulneg  42822  ltdiv23neg  42824  monoordxrv  42912  monoordxr  42913  monoord2xrv  42914  monoord2xr  42915  evthiccabs  42924  sqrlearg  42981  climinf  43037  climinff  43042  limsupres  43136  climinf2  43138  climinf2mpt  43145  climinfmpt  43146  supcnvlimsup  43171  liminfval2  43199  liminflelimsuplem  43206  liminfltlem  43235  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  iblspltprt  43404  itgspltprt  43410  stoweidlem3  43434  fourierdlem2  43540  fourierdlem3  43541  fourierdlem11  43549  fourierdlem12  43550  fourierdlem15  43553  fourierdlem34  43572  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem79  43616  fourierdlem83  43620  fourierdlem89  43626  fourierdlem91  43628  fourierdlem100  43637  fourierdlem107  43644  fourierdlem109  43646  fourierdlem112  43649  etransclem31  43696  etransclem32  43697  rrndistlt  43721  ioorrnopn  43736  ioorrnopnxrlem  43737  sge0less  43820  sge0le  43835  sge0split  43837  sge0lempt  43838  sge0iunmptlemre  43843  sge0isum  43855  sge0seq  43874  meaiuninclem  43908  meaiininclem  43914  meaiininc  43915  isome  43922  omeunile  43933  omeiunlempt  43948  carageniuncllem2  43950  0ome  43957  isomenndlem  43958  isomennd  43959  ovnsslelem  43988  ovnssle  43989  ovnsubadd  44000  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmvval0  44015  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoidmvlelem5  44027  hoidmvle  44028  hoidifhspdmvle  44048  hspmbllem2  44055  hspmbl  44057  ovnsubadd2lem  44073  ovolval4lem2  44078  ovolval4  44079  ovolval5lem2  44081  vonioolem2  44109  vonioo  44110  vonicclem2  44112  vonicc  44113  smfid  44175  smflimlem3  44195  2elfz2melfz  44698  smonoord  44711  iccpart  44756  iccpartimp  44757  iccpartres  44758  sqrtpwpw2p  44878  ismgmALT  45305  iscmgmALT  45306  issgrpALT  45307  iscsgrpALT  45308  lindslinindsimp2lem5  45691  rrx2plordisom  45957  aacllem  46391