Theorem breq12d 5120

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  breq123d  5121  3brtr3d  5138  3brtr4d  5139  sbcbr  5162  pocl  5554  csbcnvgALT  5848  cnvpo  6260  sbcfung  6540  isoeq1  7292  isocnv  7305  isotr  7311  caovordig  7594  caovordg  7596  caovord2d  7598  caovord  7600  ofrfvalg  7661  ofrval  7665  ofrfval2  7674  caofref  7684  fnwelem  8110  poseq  8137  fundmeng  9003  enrefnn  9018  xpsneng  9026  xpcomeng  9033  xpdom2g  9037  limensuc  9118  infensuc  9119  pssnn  9132  unxpdom  9200  dif1ennnALT  9222  unfilem3  9256  fodomfi  9261  domunfican  9272  fodomfiOLD  9281  marypha1lem  9384  infsupprpr  9457  wemaplem1  9499  wemaplem2  9500  wemapwe  9650  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  dmttrcl  9674  rnttrcl  9675  ttrclselem2  9679  dif1card  9963  infxpenlem  9966  nnadju  10151  pwsdompw  10156  infmap2  10170  sornom  10230  isfin5  10252  isfin6  10253  domtriomlem  10395  axdc2lem  10401  axdclem2  10473  pwcfsdom  10536  cfpwsdom  10537  alephom  10538  fpwwe2lem6  10589  fpwwe2lem8  10591  tskcard  10734  ordpipq  10895  adderpqlem  10907  mulerpqlem  10908  mulcanenq  10913  lterpq  10923  ltanq  10924  ltmnq  10925  ltaddnq  10927  ltrnq  10932  archnq  10933  reclem4pr  11003  ltasr  11053  sqgt0sr  11059  axpre-ltadd  11120  axpre-mulgt0  11121  ltadd1  11645  leadd2  11647  ltmul2  12033  lemul2  12035  lemul1a  12036  ltdiv1  12047  ltdiv2  12069  lediv2  12073  div4p1lem1div2  12437  nn0ledivnn  13066  xleadd1  13215  xltadd2  13217  xsubge0  13221  xlemul1a  13248  xlemul1  13250  xlemul2  13251  xltmul2  13253  ltdifltdiv  13796  fzennn  13933  monoord  13997  monoord2  13998  expmordi  14132  ltexp2r  14138  leexp1a  14140  sqlecan  14174  bernneq  14194  faclbnd  14255  faclbnd3  14257  faclbnd4lem1  14258  faclbnd4lem2  14259  faclbnd4lem3  14260  faclbnd4lem4  14261  faclbnd6  14264  facubnd  14265  rlimcld2  15544  isercoll2  15635  climsup  15636  iseraltlem2  15649  fsumabs  15767  fsumrlim  15777  climcndslem1  15815  climcndslem2  15816  supcvg  15822  geomulcvg  15842  cvgrat  15849  ntrivcvgtail  15866  ruclem2  16200  ruclem8  16205  addmodlteqALT  16295  fproddvdsd  16305  sadcaddlem  16427  sadcadd  16428  nn0seqcvgd  16540  algcvg  16546  algcvga  16549  eucalgcvga  16556  isprm5  16677  qnumgt0  16720  pcprendvds2  16812  pcpremul  16814  pcadd2  16861  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  2expltfac  17063  xpsle  17542  mreexexlemd  17605  issubc  17797  latjlej2  18413  latmlem2  18429  sylow1lem3  19530  isslw  19538  fislw  19555  efgi  19649  lt6abl  19825  ablfac1eu  20005  isabv  20720  abvtri  20731  psdmul  22053  cayleyhamilton1  22779  isucn  24165  ispsmet  24192  psmettri2  24197  ismet  24211  isxmet  24212  xmettri2  24228  imasdsf1olem  24261  imasf1oxmet  24263  blvalps  24273  blval  24274  comet  24401  stdbdxmet  24403  nrmmetd  24462  tngngp  24542  tngngp3  24544  nmofval  24602  nmolb2d  24606  nmoi  24616  nmoix  24617  icopnfhmeo  24841  xrhmeo  24844  evth2  24859  pi1grplem  24949  minveclem6  25334  ovolfiniun  25402  ovoliunlem3  25405  voliunlem3  25453  ioombl1  25463  mbfmax  25550  mbfpos  25552  itg1climres  25615  mbfi1fseqlem2  25617  mbfi1fseqlem6  25621  mbfi1fseq  25622  mbfmullem  25626  itg2split  25650  itg2monolem1  25651  itg2monolem3  25653  itg2mono  25654  itg2i1fseqle  25655  itg2i1fseq  25656  itg2i1fseq2  25657  itg2addlem  25659  rolle  25894  dvlip  25898  c1lip1  25902  dvcnvrelem1  25922  dvcvx  25925  ply1divex  26042  q1pval  26060  fta1glem2  26074  fta1g  26075  fta1b  26077  plydivlem3  26203  fta1lem  26215  fta1  26216  aalioulem3  26242  aalioulem4  26243  aaliou3lem2  26251  aaliou3lem8  26253  aaliou3lem9  26258  ulmdvlem1  26309  ulmdvlem3  26311  abelthlem2  26342  abelthlem7a  26347  argrege0  26520  cxplt  26603  cxplea  26605  cxple2  26606  cxplt3  26609  logbleb  26693  logblt  26694  rlimcxp  26884  scvxcvx  26896  jensenlem2  26898  ftalem3  26985  ftalem7  26989  vmalelog  27116  chtub  27123  chpchtsum  27130  bclbnd  27191  efexple  27192  bposlem5  27199  bposlem6  27200  bposlem7  27201  lgsdilem  27235  2lgslem1a2  27301  2sqreuop  27373  2sqreuopnn  27374  2sqreuoplt  27375  2sqreuopltb  27376  2sqreuopnnlt  27377  2sqreuopnnltb  27378  dchrisumlem3  27402  dchrmusumlema  27404  dchrmusum2  27405  dchrvmasumlem2  27409  dchrvmasumlema  27411  dchrvmasumiflem1  27412  dchrisum0flblem2  27420  dchrisum0flb  27421  dchrisum0lema  27425  dchrisum0lem1b  27426  dchrisum0lem2  27429  pntrlog2bndlem2  27489  pntibndlem2  27502  pntlemf  27516  ostth2lem1  27529  qabvle  27536  sltval2  27568  sltres  27574  nolesgn2o  27583  nogesgn1o  27585  nodense  27604  nolt02o  27607  nogt01o  27608  noresle  27609  nosupbnd2lem1  27627  nosupbnd2  27628  noinfbnd2lem1  27642  noinfbnd2  27643  addsproplem1  27876  addsprop  27883  sltadd2im  27893  sleadd2im  27895  sleadd1  27896  sleadd2  27897  sltadd1  27899  sltsub1  27980  sltsub2  27981  sltsubsubbd  27987  sltsubsub2bd  27988  posdifsd  28001  subsge0d  28003  mulsproplemcbv  28018  mulsproplem1  28019  mulsprop  28033  slemuld  28041  sltmul1d  28076  sltmulneg1d  28079  sltmulneg2d  28080  slemul1ad  28085  pw2gt0divsd  28328  pw2ge0divsd  28329  legso  28526  iscgra  28736  isleag  28774  iseqlg  28794  brbtwn2  28832  axlowdim  28888  ewlksfval  29529  isnvlem  30539  nvtri  30599  nmlnoubi  30725  nmblolbii  30728  nmblolbi  30729  blocnilem  30733  sii  30783  ubthlem2  30800  minvecolem3  30805  minvecolem5  30810  minvecolem6  30811  norm-ii  31067  norm3dif  31079  norm3adifi  31082  bcs  31110  pjnorm  31653  pjnel  31655  nmbdoplbi  31953  nmbdoplb  31954  nmcoplb  31959  lnconi  31962  nmbdfnlb  31979  nmcfnlb  31983  pjdifnormi  32096  mdslmd2i  32259  cvmd  32265  cvexch  32303  cdj1i  32362  cdj3lem1  32363  cdj3lem2b  32366  cdj3lem3b  32369  cdj3i  32370  isoun  32625  nexple  32769  ismnt  32909  mgcmntco  32920  dfmgc2lem  32921  dfmgc2  32922  mgcf1o  32929  ischn  32932  chnltm1  32934  chnind  32937  chnub  32938  isomnd  33015  omndadd  33020  omndmul  33028  ogrpinvlt  33037  gsumle  33038  isinftm  33135  rlocaddval  33219  rlocmulval  33220  fldext2chn  33718  constrextdg2lem  33738  constrext2chn  33749  xrmulc1cn  33920  lmdvg  33943  faeval  34236  brfae  34238  inelcarsg  34302  carsgsigalem  34306  carsgclctunlem2  34310  carsgclctun  34312  hgt750lemc  34638  hgt750lemd  34639  hgt749d  34640  sconnpht  35216  snmlval  35318  satfv1lem  35349  satfv1  35350  satfv0fun  35358  satfv0fvfmla0  35400  lediv2aALT  35664  faclim  35733  fvtransport  36020  idinside  36072  btwnconn1lem7  36081  btwnconn1lem11  36085  btwnconn1lem12  36086  ditgeq123dv  36209  cbvditgdavw2  36286  nn0prpwlem  36310  weiunlem1  36450  weiunfrlem  36452  bj-opabco  37176  poimirlem29  37643  heicant  37649  itg2addnclem  37665  itg2addnclem3  37667  itg2gt0cn  37669  ftc1anclem6  37692  ftc1anc  37695  ftc2nc  37696  dvasin  37698  areacirclem1  37702  seqpo  37741  incsequz  37742  metf1o  37749  mettrifi  37751  cntotbnd  37790  heiborlem4  37808  heiborlem6  37810  heiborlem10  37814  bfplem1  37816  bfplem2  37817  isopos  39173  oplecon3b  39193  atlatle  39313  4at2  39608  pmaple  39755  islaut  40077  lautcnvle  40083  lautco  40091  ltrncnvel  40136  cdlemeg49lebilem  40533  cdlemg17h  40662  tendoset  40753  tendotp  40755  cdlemk39s  40933  lcmineqlem23  42039  lcmineqlem  42040  intlewftc  42049  aks4d1p1p4  42059  dvle2  42060  aks4d1p8d2  42073  aks4d1p9  42076  aks4d1  42077  2ap1caineq  42133  sticksstones1  42134  sticksstones2  42135  sticksstones3  42136  sticksstones8  42141  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones15  42149  aks6d1c7lem3  42170  unitscyglem1  42183  brif12  42213  dvdsexpnn0  42322  dvdsexpb  42323  reltsub1  42374  irrapxlem2  42811  irrapxlem4  42813  irrapxlem5  42814  irrapxlem6  42815  pellexlem3  42819  monotuz  42930  monotoddzzfi  42931  monotoddzz  42932  jm2.17a  42949  jm2.17b  42950  rmygeid  42953  rmydioph  43003  expdiophlem1  43010  expdiophlem2  43011  ttac  43025  fnwe2lem2  43040  relexp01min  43702  cvgdvgrat  44302  relpeq1  44934  monoords  45295  supxrgelem  45333  supxrge  45334  abslt2sqd  45356  ltmulneg  45388  ltdiv23neg  45390  monoordxrv  45477  monoordxr  45478  monoord2xrv  45479  monoord2xr  45480  evthiccabs  45494  sqrlearg  45551  climinf  45604  climinff  45609  limsupres  45703  climinf2  45705  climinf2mpt  45712  climinfmpt  45713  supcnvlimsup  45738  liminfval2  45766  liminfltlem  45802  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  iblspltprt  45971  itgspltprt  45977  stoweidlem3  46001  fourierdlem2  46107  fourierdlem3  46108  fourierdlem11  46116  fourierdlem12  46117  fourierdlem15  46120  fourierdlem34  46139  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem79  46183  fourierdlem83  46187  fourierdlem89  46193  fourierdlem91  46195  fourierdlem100  46204  fourierdlem107  46211  fourierdlem109  46213  fourierdlem112  46216  etransclem31  46263  etransclem32  46264  rrndistlt  46288  ioorrnopn  46303  ioorrnopnxrlem  46304  sge0less  46390  sge0le  46405  sge0split  46407  sge0lempt  46408  sge0iunmptlemre  46413  sge0isum  46425  sge0seq  46444  meaiuninclem  46478  meaiininclem  46484  meaiininc  46485  isome  46492  omeunile  46503  omeiunlempt  46518  carageniuncllem2  46520  0ome  46527  isomenndlem  46528  isomennd  46529  ovnssle  46559  ovnsubadd  46570  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmvval0  46585  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hoidmvlelem5  46597  hoidmvle  46598  hoidifhspdmvle  46618  hspmbllem2  46625  hspmbl  46627  ovnsubadd2lem  46643  ovolval4lem2  46648  ovolval4  46649  ovolval5lem2  46651  vonioolem2  46679  vonioo  46680  vonicclem2  46682  vonicc  46683  smfid  46750  smflimlem3  46771  ormkglobd  46873  natglobalincr  46875  tworepnotupword  46884  squeezedltsq  46887  2elfz2melfz  47319  smonoord  47372  iccpart  47417  iccpartimp  47418  iccpartres  47419  sqrtpwpw2p  47539  grlicsym  48005  grlictr  48007  ismgmALT  48211  iscmgmALT  48212  issgrpALT  48213  iscsgrpALT  48214  lindslinindsimp2lem5  48451  rrx2plordisom  48712  aacllem  49790