Theorem breq12d 5109

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 5101	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   class class class wbr 5096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097

This theorem is referenced by:  breq123d  5110  3brtr3d  5127  3brtr4d  5128  sbcbr  5151  pocl  5538  csbcnvgALT  5831  cnvpo  6243  sbcfung  6514  isoeq1  7261  isocnv  7274  isotr  7280  caovordig  7561  caovordg  7563  caovord2d  7565  caovord  7567  ofrfvalg  7628  ofrval  7632  ofrfval2  7641  caofref  7651  fnwelem  8071  poseq  8098  fundmeng  8967  enrefnn  8981  xpsneng  8988  xpcomeng  8995  xpdom2g  8999  limensuc  9080  infensuc  9081  pssnn  9091  unxpdom  9157  dif1ennnALT  9175  unfilem3  9205  fodomfi  9210  domunfican  9220  fodomfiOLD  9228  marypha1lem  9334  infsupprpr  9407  wemaplem1  9449  wemaplem2  9450  wemapwe  9604  ssttrcl  9622  ttrcltr  9623  ttrclss  9627  dmttrcl  9628  rnttrcl  9629  ttrclselem2  9633  dif1card  9918  infxpenlem  9921  nnadju  10106  pwsdompw  10111  infmap2  10125  sornom  10185  isfin5  10207  isfin6  10208  domtriomlem  10350  axdc2lem  10356  axdclem2  10428  pwcfsdom  10492  cfpwsdom  10493  alephom  10494  fpwwe2lem6  10545  fpwwe2lem8  10547  tskcard  10690  ordpipq  10851  adderpqlem  10863  mulerpqlem  10864  mulcanenq  10869  lterpq  10879  ltanq  10880  ltmnq  10881  ltaddnq  10883  ltrnq  10888  archnq  10889  reclem4pr  10959  ltasr  11009  sqgt0sr  11015  axpre-ltadd  11076  axpre-mulgt0  11077  ltadd1  11602  leadd2  11604  ltmul2  11990  lemul2  11992  lemul1a  11993  ltdiv1  12004  ltdiv2  12026  lediv2  12030  div4p1lem1div2  12394  nn0ledivnn  13018  xleadd1  13168  xltadd2  13170  xsubge0  13174  xlemul1a  13201  xlemul1  13203  xlemul2  13204  xltmul2  13206  ltdifltdiv  13752  fzennn  13889  monoord  13953  monoord2  13954  expmordi  14088  ltexp2r  14094  leexp1a  14096  sqlecan  14130  bernneq  14150  faclbnd  14211  faclbnd3  14213  faclbnd4lem1  14214  faclbnd4lem2  14215  faclbnd4lem3  14216  faclbnd4lem4  14217  faclbnd6  14220  facubnd  14221  rlimcld2  15499  isercoll2  15590  climsup  15591  iseraltlem2  15604  fsumabs  15722  fsumrlim  15732  climcndslem1  15770  climcndslem2  15771  supcvg  15777  geomulcvg  15797  cvgrat  15804  ntrivcvgtail  15821  ruclem2  16155  ruclem8  16160  addmodlteqALT  16250  fproddvdsd  16260  sadcaddlem  16382  sadcadd  16383  nn0seqcvgd  16495  algcvg  16501  algcvga  16504  eucalgcvga  16511  isprm5  16632  qnumgt0  16675  pcprendvds2  16767  pcpremul  16769  pcadd2  16816  prmreclem4  16845  prmreclem5  16846  prmreclem6  16847  2expltfac  17018  xpsle  17498  mreexexlemd  17565  issubc  17757  latjlej2  18375  latmlem2  18391  ischn  18528  chnltm1  18530  chnind  18542  chnub  18543  sylow1lem3  19527  isslw  19535  fislw  19552  efgi  19646  lt6abl  19822  ablfac1eu  20002  isomnd  20050  omndadd  20055  omndmul  20062  ogrpinvlt  20071  gsumle  20072  isabv  20742  abvtri  20753  psdmul  22107  cayleyhamilton1  22834  isucn  24219  ispsmet  24246  psmettri2  24251  ismet  24265  isxmet  24266  xmettri2  24282  imasdsf1olem  24315  imasf1oxmet  24317  blvalps  24327  blval  24328  comet  24455  stdbdxmet  24457  nrmmetd  24516  tngngp  24596  tngngp3  24598  nmofval  24656  nmolb2d  24660  nmoi  24670  nmoix  24671  icopnfhmeo  24895  xrhmeo  24898  evth2  24913  pi1grplem  25003  minveclem6  25388  ovolfiniun  25456  ovoliunlem3  25459  voliunlem3  25507  ioombl1  25517  mbfmax  25604  mbfpos  25606  itg1climres  25669  mbfi1fseqlem2  25671  mbfi1fseqlem6  25675  mbfi1fseq  25676  mbfmullem  25680  itg2split  25704  itg2monolem1  25705  itg2monolem3  25707  itg2mono  25708  itg2i1fseqle  25709  itg2i1fseq  25710  itg2i1fseq2  25711  itg2addlem  25713  rolle  25948  dvlip  25952  c1lip1  25956  dvcnvrelem1  25976  dvcvx  25979  ply1divex  26096  q1pval  26114  fta1glem2  26128  fta1g  26129  fta1b  26131  plydivlem3  26257  fta1lem  26269  fta1  26270  aalioulem3  26296  aalioulem4  26297  aaliou3lem2  26305  aaliou3lem8  26307  aaliou3lem9  26312  ulmdvlem1  26363  ulmdvlem3  26365  abelthlem2  26396  abelthlem7a  26401  argrege0  26574  cxplt  26657  cxplea  26659  cxple2  26660  cxplt3  26663  logbleb  26747  logblt  26748  rlimcxp  26938  scvxcvx  26950  jensenlem2  26952  ftalem3  27039  ftalem7  27043  vmalelog  27170  chtub  27177  chpchtsum  27184  bclbnd  27245  efexple  27246  bposlem5  27253  bposlem6  27254  bposlem7  27255  lgsdilem  27289  2lgslem1a2  27355  2sqreuop  27427  2sqreuopnn  27428  2sqreuoplt  27429  2sqreuopltb  27430  2sqreuopnnlt  27431  2sqreuopnnltb  27432  dchrisumlem3  27456  dchrmusumlema  27458  dchrmusum2  27459  dchrvmasumlem2  27463  dchrvmasumlema  27465  dchrvmasumiflem1  27466  dchrisum0flblem2  27474  dchrisum0flb  27475  dchrisum0lema  27479  dchrisum0lem1b  27480  dchrisum0lem2  27483  pntrlog2bndlem2  27543  pntibndlem2  27556  pntlemf  27570  ostth2lem1  27583  qabvle  27590  sltval2  27622  sltres  27628  nolesgn2o  27637  nogesgn1o  27639  nodense  27658  nolt02o  27661  nogt01o  27662  noresle  27663  nosupbnd2lem1  27681  nosupbnd2  27682  noinfbnd2lem1  27696  noinfbnd2  27697  addsproplem1  27939  addsprop  27946  sltadd2im  27956  sleadd2im  27958  sleadd1  27959  sleadd2  27960  sltadd1  27962  sltsub1  28045  sltsub2  28046  sltsubsubbd  28052  sltsubsub2bd  28053  posdifsd  28067  subsge0d  28069  mulsproplemcbv  28084  mulsproplem1  28085  mulsprop  28099  slemuld  28107  sltmul1d  28142  sltmulneg1d  28145  sltmulneg2d  28146  slemul1ad  28151  zsoring  28367  pw2gt0divsd  28403  pw2ge0divsd  28404  legso  28620  iscgra  28830  isleag  28868  iseqlg  28888  brbtwn2  28927  axlowdim  28983  ewlksfval  29624  isnvlem  30634  nvtri  30694  nmlnoubi  30820  nmblolbii  30823  nmblolbi  30824  blocnilem  30828  sii  30878  ubthlem2  30895  minvecolem3  30900  minvecolem5  30905  minvecolem6  30906  norm-ii  31162  norm3dif  31174  norm3adifi  31177  bcs  31205  pjnorm  31748  pjnel  31750  nmbdoplbi  32048  nmbdoplb  32049  nmcoplb  32054  lnconi  32057  nmbdfnlb  32074  nmcfnlb  32078  pjdifnormi  32191  mdslmd2i  32354  cvmd  32360  cvexch  32398  cdj1i  32457  cdj3lem1  32458  cdj3lem2b  32461  cdj3lem3b  32464  cdj3i  32465  fnfvor  32636  ofrco  32637  isoun  32730  nexple  32874  ismnt  33014  mgcmntco  33025  dfmgc2lem  33026  dfmgc2  33027  mgcf1o  33034  isinftm  33212  rlocaddval  33299  rlocmulval  33300  fldext2chn  33834  constrextdg2lem  33854  constrext2chn  33865  xrmulc1cn  34036  lmdvg  34059  faeval  34352  brfae  34354  inelcarsg  34417  carsgsigalem  34421  carsgclctunlem2  34425  carsgclctun  34427  hgt750lemc  34753  hgt750lemd  34754  hgt749d  34755  fineqvnttrclse  35229  sconnpht  35372  snmlval  35474  satfv1lem  35505  satfv1  35506  satfv0fun  35514  satfv0fvfmla0  35556  lediv2aALT  35820  faclim  35889  fvtransport  36175  idinside  36227  btwnconn1lem7  36236  btwnconn1lem11  36240  btwnconn1lem12  36241  ditgeq123dv  36364  cbvditgdavw2  36441  nn0prpwlem  36465  weiunlem1  36605  weiunfrlem  36607  bj-opabco  37332  poimirlem29  37789  heicant  37795  itg2addnclem  37811  itg2addnclem3  37813  itg2gt0cn  37815  ftc1anclem6  37838  ftc1anc  37841  ftc2nc  37842  dvasin  37844  areacirclem1  37848  seqpo  37887  incsequz  37888  metf1o  37895  mettrifi  37897  cntotbnd  37936  heiborlem4  37954  heiborlem6  37956  heiborlem10  37960  bfplem1  37962  bfplem2  37963  isopos  39379  oplecon3b  39399  atlatle  39519  4at2  39813  pmaple  39960  islaut  40282  lautcnvle  40288  lautco  40296  ltrncnvel  40341  cdlemeg49lebilem  40738  cdlemg17h  40867  tendoset  40958  tendotp  40960  cdlemk39s  41138  lcmineqlem23  42244  lcmineqlem  42245  intlewftc  42254  aks4d1p1p4  42264  dvle2  42265  aks4d1p8d2  42278  aks4d1p9  42281  aks4d1  42282  2ap1caineq  42338  sticksstones1  42339  sticksstones2  42340  sticksstones3  42341  sticksstones8  42346  sticksstones10  42348  sticksstones11  42349  sticksstones12a  42350  sticksstones15  42354  aks6d1c7lem3  42375  unitscyglem1  42388  brif12  42423  dvdsexpnn0  42531  dvdsexpb  42532  reltsub1  42583  irrapxlem2  43007  irrapxlem4  43009  irrapxlem5  43010  irrapxlem6  43011  pellexlem3  43015  monotuz  43125  monotoddzzfi  43126  monotoddzz  43127  jm2.17a  43144  jm2.17b  43145  rmygeid  43148  rmydioph  43198  expdiophlem1  43205  expdiophlem2  43206  ttac  43220  fnwe2lem2  43235  relexp01min  43896  cvgdvgrat  44496  relpeq1  45127  monoords  45487  supxrgelem  45524  supxrge  45525  abslt2sqd  45547  ltmulneg  45578  ltdiv23neg  45580  monoordxrv  45667  monoordxr  45668  monoord2xrv  45669  monoord2xr  45670  evthiccabs  45684  sqrlearg  45741  climinf  45794  climinff  45799  limsupres  45891  climinf2  45893  climinf2mpt  45900  climinfmpt  45901  supcnvlimsup  45926  liminfval2  45954  liminfltlem  45990  fprodsubrecnncnvlem  46093  fprodaddrecnncnvlem  46095  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  iblspltprt  46159  itgspltprt  46165  stoweidlem3  46189  fourierdlem2  46295  fourierdlem3  46296  fourierdlem11  46304  fourierdlem12  46305  fourierdlem15  46308  fourierdlem34  46327  fourierdlem41  46334  fourierdlem48  46340  fourierdlem49  46341  fourierdlem79  46371  fourierdlem83  46375  fourierdlem89  46381  fourierdlem91  46383  fourierdlem100  46392  fourierdlem107  46399  fourierdlem109  46401  fourierdlem112  46404  etransclem31  46451  etransclem32  46452  rrndistlt  46476  ioorrnopn  46491  ioorrnopnxrlem  46492  sge0less  46578  sge0le  46593  sge0split  46595  sge0lempt  46596  sge0iunmptlemre  46601  sge0isum  46613  sge0seq  46632  meaiuninclem  46666  meaiininclem  46672  meaiininc  46673  isome  46680  omeunile  46691  omeiunlempt  46706  carageniuncllem2  46708  0ome  46715  isomenndlem  46716  isomennd  46717  ovnssle  46747  ovnsubadd  46758  hsphoidmvle2  46771  hsphoidmvle  46772  hoidmvval0  46773  hoidmv1lelem1  46777  hoidmv1lelem2  46778  hoidmv1lelem3  46779  hoidmv1le  46780  hoidmvlelem1  46781  hoidmvlelem2  46782  hoidmvlelem3  46783  hoidmvlelem4  46784  hoidmvlelem5  46785  hoidmvle  46786  hoidifhspdmvle  46806  hspmbllem2  46813  hspmbl  46815  ovnsubadd2lem  46831  ovolval4lem2  46836  ovolval4  46837  ovolval5lem2  46839  vonioolem2  46867  vonioo  46868  vonicclem2  46870  vonicc  46871  smfid  46938  smflimlem3  46959  ormkglobd  47061  natglobalincr  47063  chnerlem1  47068  squeezedltsq  47074  2elfz2melfz  47506  smonoord  47559  iccpart  47604  iccpartimp  47605  iccpartres  47606  sqrtpwpw2p  47726  grlicsym  48201  grlictr  48203  ismgmALT  48411  iscmgmALT  48412  issgrpALT  48413  iscsgrpALT  48414  lindslinindsimp2lem5  48650  rrx2plordisom  48911  aacllem  49988