Theorem breq12d 5102

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  breq123d  5103  3brtr3d  5120  3brtr4d  5121  sbcbr  5144  pocl  5530  csbcnvgALT  5823  cnvpo  6234  sbcfung  6505  isoeq1  7251  isocnv  7264  isotr  7270  caovordig  7551  caovordg  7553  caovord2d  7555  caovord  7557  ofrfvalg  7618  ofrval  7622  ofrfval2  7631  caofref  7641  fnwelem  8061  poseq  8088  fundmeng  8954  enrefnn  8968  xpsneng  8975  xpcomeng  8982  xpdom2g  8986  limensuc  9067  infensuc  9068  pssnn  9078  unxpdom  9143  dif1ennnALT  9161  unfilem3  9191  fodomfi  9196  domunfican  9206  fodomfiOLD  9214  marypha1lem  9317  infsupprpr  9390  wemaplem1  9432  wemaplem2  9433  wemapwe  9587  ssttrcl  9605  ttrcltr  9606  ttrclss  9610  dmttrcl  9611  rnttrcl  9612  ttrclselem2  9616  dif1card  9901  infxpenlem  9904  nnadju  10089  pwsdompw  10094  infmap2  10108  sornom  10168  isfin5  10190  isfin6  10191  domtriomlem  10333  axdc2lem  10339  axdclem2  10411  pwcfsdom  10474  cfpwsdom  10475  alephom  10476  fpwwe2lem6  10527  fpwwe2lem8  10529  tskcard  10672  ordpipq  10833  adderpqlem  10845  mulerpqlem  10846  mulcanenq  10851  lterpq  10861  ltanq  10862  ltmnq  10863  ltaddnq  10865  ltrnq  10870  archnq  10871  reclem4pr  10941  ltasr  10991  sqgt0sr  10997  axpre-ltadd  11058  axpre-mulgt0  11059  ltadd1  11584  leadd2  11586  ltmul2  11972  lemul2  11974  lemul1a  11975  ltdiv1  11986  ltdiv2  12008  lediv2  12012  div4p1lem1div2  12376  nn0ledivnn  13005  xleadd1  13154  xltadd2  13156  xsubge0  13160  xlemul1a  13187  xlemul1  13189  xlemul2  13190  xltmul2  13192  ltdifltdiv  13738  fzennn  13875  monoord  13939  monoord2  13940  expmordi  14074  ltexp2r  14080  leexp1a  14082  sqlecan  14116  bernneq  14136  faclbnd  14197  faclbnd3  14199  faclbnd4lem1  14200  faclbnd4lem2  14201  faclbnd4lem3  14202  faclbnd4lem4  14203  faclbnd6  14206  facubnd  14207  rlimcld2  15485  isercoll2  15576  climsup  15577  iseraltlem2  15590  fsumabs  15708  fsumrlim  15718  climcndslem1  15756  climcndslem2  15757  supcvg  15763  geomulcvg  15783  cvgrat  15790  ntrivcvgtail  15807  ruclem2  16141  ruclem8  16146  addmodlteqALT  16236  fproddvdsd  16246  sadcaddlem  16368  sadcadd  16369  nn0seqcvgd  16481  algcvg  16487  algcvga  16490  eucalgcvga  16497  isprm5  16618  qnumgt0  16661  pcprendvds2  16753  pcpremul  16755  pcadd2  16802  prmreclem4  16831  prmreclem5  16832  prmreclem6  16833  2expltfac  17004  xpsle  17483  mreexexlemd  17550  issubc  17742  latjlej2  18360  latmlem2  18376  ischn  18513  chnltm1  18515  chnind  18527  chnub  18528  sylow1lem3  19512  isslw  19520  fislw  19537  efgi  19631  lt6abl  19807  ablfac1eu  19987  isomnd  20035  omndadd  20040  omndmul  20047  ogrpinvlt  20056  gsumle  20057  isabv  20726  abvtri  20737  psdmul  22081  cayleyhamilton1  22807  isucn  24192  ispsmet  24219  psmettri2  24224  ismet  24238  isxmet  24239  xmettri2  24255  imasdsf1olem  24288  imasf1oxmet  24290  blvalps  24300  blval  24301  comet  24428  stdbdxmet  24430  nrmmetd  24489  tngngp  24569  tngngp3  24571  nmofval  24629  nmolb2d  24633  nmoi  24643  nmoix  24644  icopnfhmeo  24868  xrhmeo  24871  evth2  24886  pi1grplem  24976  minveclem6  25361  ovolfiniun  25429  ovoliunlem3  25432  voliunlem3  25480  ioombl1  25490  mbfmax  25577  mbfpos  25579  itg1climres  25642  mbfi1fseqlem2  25644  mbfi1fseqlem6  25648  mbfi1fseq  25649  mbfmullem  25653  itg2split  25677  itg2monolem1  25678  itg2monolem3  25680  itg2mono  25681  itg2i1fseqle  25682  itg2i1fseq  25683  itg2i1fseq2  25684  itg2addlem  25686  rolle  25921  dvlip  25925  c1lip1  25929  dvcnvrelem1  25949  dvcvx  25952  ply1divex  26069  q1pval  26087  fta1glem2  26101  fta1g  26102  fta1b  26104  plydivlem3  26230  fta1lem  26242  fta1  26243  aalioulem3  26269  aalioulem4  26270  aaliou3lem2  26278  aaliou3lem8  26280  aaliou3lem9  26285  ulmdvlem1  26336  ulmdvlem3  26338  abelthlem2  26369  abelthlem7a  26374  argrege0  26547  cxplt  26630  cxplea  26632  cxple2  26633  cxplt3  26636  logbleb  26720  logblt  26721  rlimcxp  26911  scvxcvx  26923  jensenlem2  26925  ftalem3  27012  ftalem7  27016  vmalelog  27143  chtub  27150  chpchtsum  27157  bclbnd  27218  efexple  27219  bposlem5  27226  bposlem6  27227  bposlem7  27228  lgsdilem  27262  2lgslem1a2  27328  2sqreuop  27400  2sqreuopnn  27401  2sqreuoplt  27402  2sqreuopltb  27403  2sqreuopnnlt  27404  2sqreuopnnltb  27405  dchrisumlem3  27429  dchrmusumlema  27431  dchrmusum2  27432  dchrvmasumlem2  27436  dchrvmasumlema  27438  dchrvmasumiflem1  27439  dchrisum0flblem2  27447  dchrisum0flb  27448  dchrisum0lema  27452  dchrisum0lem1b  27453  dchrisum0lem2  27456  pntrlog2bndlem2  27516  pntibndlem2  27529  pntlemf  27543  ostth2lem1  27556  qabvle  27563  sltval2  27595  sltres  27601  nolesgn2o  27610  nogesgn1o  27612  nodense  27631  nolt02o  27634  nogt01o  27635  noresle  27636  nosupbnd2lem1  27654  nosupbnd2  27655  noinfbnd2lem1  27669  noinfbnd2  27670  addsproplem1  27912  addsprop  27919  sltadd2im  27929  sleadd2im  27931  sleadd1  27932  sleadd2  27933  sltadd1  27935  sltsub1  28016  sltsub2  28017  sltsubsubbd  28023  sltsubsub2bd  28024  posdifsd  28037  subsge0d  28039  mulsproplemcbv  28054  mulsproplem1  28055  mulsprop  28069  slemuld  28077  sltmul1d  28112  sltmulneg1d  28115  sltmulneg2d  28116  slemul1ad  28121  zsoring  28332  pw2gt0divsd  28368  pw2ge0divsd  28369  legso  28577  iscgra  28787  isleag  28825  iseqlg  28845  brbtwn2  28883  axlowdim  28939  ewlksfval  29580  isnvlem  30590  nvtri  30650  nmlnoubi  30776  nmblolbii  30779  nmblolbi  30780  blocnilem  30784  sii  30834  ubthlem2  30851  minvecolem3  30856  minvecolem5  30861  minvecolem6  30862  norm-ii  31118  norm3dif  31130  norm3adifi  31133  bcs  31161  pjnorm  31704  pjnel  31706  nmbdoplbi  32004  nmbdoplb  32005  nmcoplb  32010  lnconi  32013  nmbdfnlb  32030  nmcfnlb  32034  pjdifnormi  32147  mdslmd2i  32310  cvmd  32316  cvexch  32354  cdj1i  32413  cdj3lem1  32414  cdj3lem2b  32417  cdj3lem3b  32420  cdj3i  32421  fnfvor  32592  ofrco  32593  isoun  32683  nexple  32827  ismnt  32964  mgcmntco  32975  dfmgc2lem  32976  dfmgc2  32977  mgcf1o  32984  isinftm  33150  rlocaddval  33235  rlocmulval  33236  fldext2chn  33741  constrextdg2lem  33761  constrext2chn  33772  xrmulc1cn  33943  lmdvg  33966  faeval  34259  brfae  34261  inelcarsg  34324  carsgsigalem  34328  carsgclctunlem2  34332  carsgclctun  34334  hgt750lemc  34660  hgt750lemd  34661  hgt749d  34662  fineqvnttrclse  35144  sconnpht  35273  snmlval  35375  satfv1lem  35406  satfv1  35407  satfv0fun  35415  satfv0fvfmla0  35457  lediv2aALT  35721  faclim  35790  fvtransport  36076  idinside  36128  btwnconn1lem7  36137  btwnconn1lem11  36141  btwnconn1lem12  36142  ditgeq123dv  36265  cbvditgdavw2  36342  nn0prpwlem  36366  weiunlem1  36506  weiunfrlem  36508  bj-opabco  37232  poimirlem29  37699  heicant  37705  itg2addnclem  37721  itg2addnclem3  37723  itg2gt0cn  37725  ftc1anclem6  37748  ftc1anc  37751  ftc2nc  37752  dvasin  37754  areacirclem1  37758  seqpo  37797  incsequz  37798  metf1o  37805  mettrifi  37807  cntotbnd  37846  heiborlem4  37864  heiborlem6  37866  heiborlem10  37870  bfplem1  37872  bfplem2  37873  isopos  39289  oplecon3b  39309  atlatle  39429  4at2  39723  pmaple  39870  islaut  40192  lautcnvle  40198  lautco  40206  ltrncnvel  40251  cdlemeg49lebilem  40648  cdlemg17h  40777  tendoset  40868  tendotp  40870  cdlemk39s  41048  lcmineqlem23  42154  lcmineqlem  42155  intlewftc  42164  aks4d1p1p4  42174  dvle2  42175  aks4d1p8d2  42188  aks4d1p9  42191  aks4d1  42192  2ap1caineq  42248  sticksstones1  42249  sticksstones2  42250  sticksstones3  42251  sticksstones8  42256  sticksstones10  42258  sticksstones11  42259  sticksstones12a  42260  sticksstones15  42264  aks6d1c7lem3  42285  unitscyglem1  42298  brif12  42328  dvdsexpnn0  42437  dvdsexpb  42438  reltsub1  42489  irrapxlem2  42926  irrapxlem4  42928  irrapxlem5  42929  irrapxlem6  42930  pellexlem3  42934  monotuz  43044  monotoddzzfi  43045  monotoddzz  43046  jm2.17a  43063  jm2.17b  43064  rmygeid  43067  rmydioph  43117  expdiophlem1  43124  expdiophlem2  43125  ttac  43139  fnwe2lem2  43154  relexp01min  43816  cvgdvgrat  44416  relpeq1  45047  monoords  45408  supxrgelem  45446  supxrge  45447  abslt2sqd  45469  ltmulneg  45500  ltdiv23neg  45502  monoordxrv  45589  monoordxr  45590  monoord2xrv  45591  monoord2xr  45592  evthiccabs  45606  sqrlearg  45663  climinf  45716  climinff  45721  limsupres  45813  climinf2  45815  climinf2mpt  45822  climinfmpt  45823  supcnvlimsup  45848  liminfval2  45876  liminfltlem  45912  fprodsubrecnncnvlem  46015  fprodaddrecnncnvlem  46017  ioodvbdlimc1lem1  46039  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  iblspltprt  46081  itgspltprt  46087  stoweidlem3  46111  fourierdlem2  46217  fourierdlem3  46218  fourierdlem11  46226  fourierdlem12  46227  fourierdlem15  46230  fourierdlem34  46249  fourierdlem41  46256  fourierdlem48  46262  fourierdlem49  46263  fourierdlem79  46293  fourierdlem83  46297  fourierdlem89  46303  fourierdlem91  46305  fourierdlem100  46314  fourierdlem107  46321  fourierdlem109  46323  fourierdlem112  46326  etransclem31  46373  etransclem32  46374  rrndistlt  46398  ioorrnopn  46413  ioorrnopnxrlem  46414  sge0less  46500  sge0le  46515  sge0split  46517  sge0lempt  46518  sge0iunmptlemre  46523  sge0isum  46535  sge0seq  46554  meaiuninclem  46588  meaiininclem  46594  meaiininc  46595  isome  46602  omeunile  46613  omeiunlempt  46628  carageniuncllem2  46630  0ome  46637  isomenndlem  46638  isomennd  46639  ovnssle  46669  ovnsubadd  46680  hsphoidmvle2  46693  hsphoidmvle  46694  hoidmvval0  46695  hoidmv1lelem1  46699  hoidmv1lelem2  46700  hoidmv1lelem3  46701  hoidmv1le  46702  hoidmvlelem1  46703  hoidmvlelem2  46704  hoidmvlelem3  46705  hoidmvlelem4  46706  hoidmvlelem5  46707  hoidmvle  46708  hoidifhspdmvle  46728  hspmbllem2  46735  hspmbl  46737  ovnsubadd2lem  46753  ovolval4lem2  46758  ovolval4  46759  ovolval5lem2  46761  vonioolem2  46789  vonioo  46790  vonicclem2  46792  vonicc  46793  smfid  46860  smflimlem3  46881  ormkglobd  46983  natglobalincr  46985  chnerlem1  46990  squeezedltsq  46996  2elfz2melfz  47428  smonoord  47481  iccpart  47526  iccpartimp  47527  iccpartres  47528  sqrtpwpw2p  47648  grlicsym  48123  grlictr  48125  ismgmALT  48333  iscmgmALT  48334  issgrpALT  48335  iscsgrpALT  48336  lindslinindsimp2lem5  48573  rrx2plordisom  48834  aacllem  49912