Theorem breq12d 5165

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   class class class wbr 5152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153

This theorem is referenced by:  breq123d  5166  3brtr3d  5183  3brtr4d  5184  sbcbr  5207  pocl  5600  poclOLD  5601  csbcnvgALT  5890  cnvpo  6297  sbcfung  6582  isoeq1  7328  isocnv  7341  isotr  7347  caovordig  7630  caovordg  7632  caovord2d  7634  caovord  7636  ofrfvalg  7697  ofrval  7701  ofrfval2  7710  caofref  7719  fnwelem  8144  poseq  8171  fundmeng  9067  enrefnn  9084  xpsneng  9093  xpcomeng  9101  xpdom2g  9105  limensuc  9191  infensuc  9192  pssnn  9205  unxpdom  9290  pssnnOLD  9302  dif1ennnALT  9314  unfilem3  9349  unfiOLD  9350  domunfican  9358  fodomfi  9365  marypha1lem  9472  infsupprpr  9543  wemaplem1  9585  wemaplem2  9586  wemapwe  9736  ssttrcl  9754  ttrcltr  9755  ttrclss  9759  dmttrcl  9760  rnttrcl  9761  ttrclselem2  9765  dif1card  10049  infxpenlem  10052  nnadju  10236  pwsdompw  10243  infmap2  10257  sornom  10316  isfin5  10338  isfin6  10339  domtriomlem  10481  axdc2lem  10487  axdclem2  10559  pwcfsdom  10622  cfpwsdom  10623  alephom  10624  fpwwe2lem6  10675  fpwwe2lem8  10677  tskcard  10820  ordpipq  10981  adderpqlem  10993  mulerpqlem  10994  mulcanenq  10999  lterpq  11009  ltanq  11010  ltmnq  11011  ltaddnq  11013  ltrnq  11018  archnq  11019  reclem4pr  11089  ltasr  11139  sqgt0sr  11145  axpre-ltadd  11206  axpre-mulgt0  11207  ltadd1  11727  leadd2  11729  ltmul2  12112  lemul2  12114  lemul1a  12115  ltdiv1  12125  ltdiv2  12147  lediv2  12151  div4p1lem1div2  12514  nn0ledivnn  13136  xleadd1  13283  xltadd2  13285  xsubge0  13289  xlemul1a  13316  xlemul1  13318  xlemul2  13319  xltmul2  13321  ltdifltdiv  13849  fzennn  13983  monoord  14047  monoord2  14048  expmordi  14181  ltexp2r  14187  leexp1a  14189  sqlecan  14222  bernneq  14241  faclbnd  14302  faclbnd3  14304  faclbnd4lem1  14305  faclbnd4lem2  14306  faclbnd4lem3  14307  faclbnd4lem4  14308  faclbnd6  14311  facubnd  14312  rlimcld2  15575  isercoll2  15668  climsup  15669  iseraltlem2  15682  fsumabs  15800  fsumrlim  15810  climcndslem1  15848  climcndslem2  15849  supcvg  15855  geomulcvg  15875  cvgrat  15882  ntrivcvgtail  15899  ruclem2  16229  ruclem8  16234  addmodlteqALT  16322  fproddvdsd  16332  sadcaddlem  16452  sadcadd  16453  nn0seqcvgd  16566  algcvg  16572  algcvga  16575  eucalgcvga  16582  isprm5  16703  qnumgt0  16747  pcprendvds2  16838  pcpremul  16840  pcadd2  16887  prmreclem4  16916  prmreclem5  16917  prmreclem6  16918  2expltfac  17090  xpsle  17589  mreexexlemd  17652  issubc  17849  latjlej2  18474  latmlem2  18490  sylow1lem3  19593  isslw  19601  fislw  19618  efgi  19712  lt6abl  19888  ablfac1eu  20068  isabv  20739  abvtri  20750  psdmul  22152  cayleyhamilton1  22877  isucn  24266  ispsmet  24293  psmettri2  24298  ismet  24312  isxmet  24313  xmettri2  24329  imasdsf1olem  24362  imasf1oxmet  24364  blvalps  24374  blval  24375  comet  24505  stdbdxmet  24507  nrmmetd  24566  tngngp  24654  tngngp3  24656  nmofval  24714  nmolb2d  24718  nmoi  24728  nmoix  24729  icopnfhmeo  24951  xrhmeo  24954  evth2  24969  pi1grplem  25059  minveclem6  25445  ovolfiniun  25513  ovoliunlem3  25516  voliunlem3  25564  ioombl1  25574  mbfmax  25661  mbfpos  25663  itg1climres  25727  mbfi1fseqlem2  25729  mbfi1fseqlem6  25733  mbfi1fseq  25734  mbfmullem  25738  itg2split  25762  itg2monolem1  25763  itg2monolem3  25765  itg2mono  25766  itg2i1fseqle  25767  itg2i1fseq  25768  itg2i1fseq2  25769  itg2addlem  25771  rolle  26005  dvlip  26009  c1lip1  26013  dvcnvrelem1  26033  dvcvx  26036  ply1divex  26156  q1pval  26174  fta1glem2  26188  fta1g  26189  fta1b  26191  plydivlem3  26315  fta1lem  26327  fta1  26328  aalioulem3  26354  aalioulem4  26355  aaliou3lem2  26363  aaliou3lem8  26365  aaliou3lem9  26370  ulmdvlem1  26421  ulmdvlem3  26423  abelthlem2  26454  abelthlem7a  26459  argrege0  26630  cxplt  26713  cxplea  26715  cxple2  26716  cxplt3  26719  logbleb  26803  logblt  26804  rlimcxp  26994  scvxcvx  27006  jensenlem2  27008  ftalem3  27095  ftalem7  27099  vmalelog  27226  chtub  27233  chpchtsum  27240  bclbnd  27301  efexple  27302  bposlem5  27309  bposlem6  27310  bposlem7  27311  lgsdilem  27345  2lgslem1a2  27411  2sqreuop  27483  2sqreuopnn  27484  2sqreuoplt  27485  2sqreuopltb  27486  2sqreuopnnlt  27487  2sqreuopnnltb  27488  dchrisumlem3  27512  dchrmusumlema  27514  dchrmusum2  27515  dchrvmasumlem2  27519  dchrvmasumlema  27521  dchrvmasumiflem1  27522  dchrisum0flblem2  27530  dchrisum0flb  27531  dchrisum0lema  27535  dchrisum0lem1b  27536  dchrisum0lem2  27539  pntrlog2bndlem2  27599  pntibndlem2  27612  pntlemf  27626  ostth2lem1  27639  qabvle  27646  sltval2  27678  sltres  27684  nolesgn2o  27693  nogesgn1o  27695  nodense  27714  nolt02o  27717  nogt01o  27718  noresle  27719  nosupbnd2lem1  27737  nosupbnd2  27738  noinfbnd2lem1  27752  noinfbnd2  27753  addsproplem1  27975  addsprop  27982  sltadd2im  27992  sleadd2im  27994  sleadd1  27995  sleadd2  27996  sltadd1  27998  sltsub1  28075  sltsub2  28076  sltsubsubbd  28082  sltsubsub2bd  28083  posdifsd  28096  subsge0d  28098  mulsproplemcbv  28108  mulsproplem1  28109  mulsprop  28123  slemuld  28131  sltmul1d  28166  sltmulneg1d  28169  sltmulneg2d  28170  slemul1ad  28175  legso  28518  iscgra  28728  isleag  28766  iseqlg  28786  brbtwn2  28831  axlowdim  28887  ewlksfval  29530  isnvlem  30535  nvtri  30595  nmlnoubi  30721  nmblolbii  30724  nmblolbi  30725  blocnilem  30729  sii  30779  ubthlem2  30796  minvecolem3  30801  minvecolem5  30806  minvecolem6  30807  norm-ii  31063  norm3dif  31075  norm3adifi  31078  bcs  31106  pjnorm  31649  pjnel  31651  nmbdoplbi  31949  nmbdoplb  31950  nmcoplb  31955  lnconi  31958  nmbdfnlb  31975  nmcfnlb  31979  pjdifnormi  32092  mdslmd2i  32255  cvmd  32261  cvexch  32299  cdj1i  32358  cdj3lem1  32359  cdj3lem2b  32362  cdj3lem3b  32365  cdj3i  32366  isoun  32604  ismnt  32841  mgcmntco  32852  dfmgc2lem  32853  dfmgc2  32854  mgcf1o  32861  isomnd  32913  omndadd  32918  omndmul  32926  ogrpinvlt  32935  gsumle  32936  isinftm  33023  rlocaddval  33100  rlocmulval  33101  xrmulc1cn  33701  lmdvg  33724  nexple  33798  faeval  34035  brfae  34037  inelcarsg  34101  carsgsigalem  34105  carsgclctunlem2  34109  carsgclctun  34111  hgt750lemc  34449  hgt750lemd  34450  hgt749d  34451  sconnpht  35009  snmlval  35111  satfv1lem  35142  satfv1  35143  satfv0fun  35151  satfv0fvfmla0  35193  lediv2aALT  35457  faclim  35516  fvtransport  35804  idinside  35856  btwnconn1lem7  35865  btwnconn1lem11  35869  btwnconn1lem12  35870  nn0prpwlem  35982  bj-opabco  36843  poimirlem29  37298  heicant  37304  itg2addnclem  37320  itg2addnclem3  37322  itg2gt0cn  37324  ftc1anclem6  37347  ftc1anc  37350  ftc2nc  37351  dvasin  37353  areacirclem1  37357  seqpo  37396  incsequz  37397  metf1o  37404  mettrifi  37406  cntotbnd  37445  heiborlem4  37463  heiborlem6  37465  heiborlem10  37469  bfplem1  37471  bfplem2  37472  isopos  38826  oplecon3b  38846  atlatle  38966  4at2  39261  pmaple  39408  islaut  39730  lautcnvle  39736  lautco  39744  ltrncnvel  39789  cdlemeg49lebilem  40186  cdlemg17h  40315  tendoset  40406  tendotp  40408  cdlemk39s  40586  lcmineqlem23  41698  lcmineqlem  41699  intlewftc  41708  aks4d1p1p4  41718  dvle2  41719  aks4d1p8d2  41732  aks4d1p9  41735  aks4d1  41736  2ap1caineq  41791  sticksstones1  41792  sticksstones2  41793  sticksstones3  41794  sticksstones8  41799  sticksstones10  41801  sticksstones11  41802  sticksstones12a  41803  sticksstones15  41807  aks6d1c7lem3  41828  factwoffsmonot  41871  brif12  41890  dvdsexpnn0  42071  dvdsexpb  42072  reltsub1  42108  irrapxlem2  42417  irrapxlem4  42419  irrapxlem5  42420  irrapxlem6  42421  pellexlem3  42425  monotuz  42536  monotoddzzfi  42537  monotoddzz  42538  jm2.17a  42555  jm2.17b  42556  rmygeid  42559  rmydioph  42609  expdiophlem1  42616  expdiophlem2  42617  ttac  42631  fnwe2lem2  42649  relexp01min  43317  cvgdvgrat  43924  monoords  44849  supxrgelem  44889  supxrge  44890  abslt2sqd  44912  ltmulneg  44944  ltdiv23neg  44946  monoordxrv  45034  monoordxr  45035  monoord2xrv  45036  monoord2xr  45037  evthiccabs  45051  sqrlearg  45108  climinf  45164  climinff  45169  limsupres  45263  climinf2  45265  climinf2mpt  45272  climinfmpt  45273  supcnvlimsup  45298  liminfval2  45326  liminflelimsuplem  45333  liminfltlem  45362  fprodsubrecnncnvlem  45465  fprodaddrecnncnvlem  45467  ioodvbdlimc1lem1  45489  ioodvbdlimc1lem2  45490  ioodvbdlimc2lem  45492  iblspltprt  45531  itgspltprt  45537  stoweidlem3  45561  fourierdlem2  45667  fourierdlem3  45668  fourierdlem11  45676  fourierdlem12  45677  fourierdlem15  45680  fourierdlem34  45699  fourierdlem41  45706  fourierdlem48  45712  fourierdlem49  45713  fourierdlem79  45743  fourierdlem83  45747  fourierdlem89  45753  fourierdlem91  45755  fourierdlem100  45764  fourierdlem107  45771  fourierdlem109  45773  fourierdlem112  45776  etransclem31  45823  etransclem32  45824  rrndistlt  45848  ioorrnopn  45863  ioorrnopnxrlem  45864  sge0less  45950  sge0le  45965  sge0split  45967  sge0lempt  45968  sge0iunmptlemre  45973  sge0isum  45985  sge0seq  46004  meaiuninclem  46038  meaiininclem  46044  meaiininc  46045  isome  46052  omeunile  46063  omeiunlempt  46078  carageniuncllem2  46080  0ome  46087  isomenndlem  46088  isomennd  46089  ovnssle  46119  ovnsubadd  46130  hsphoidmvle2  46143  hsphoidmvle  46144  hoidmvval0  46145  hoidmv1lelem1  46149  hoidmv1lelem2  46150  hoidmv1lelem3  46151  hoidmv1le  46152  hoidmvlelem1  46153  hoidmvlelem2  46154  hoidmvlelem3  46155  hoidmvlelem4  46156  hoidmvlelem5  46157  hoidmvle  46158  hoidifhspdmvle  46178  hspmbllem2  46185  hspmbl  46187  ovnsubadd2lem  46203  ovolval4lem2  46208  ovolval4  46209  ovolval5lem2  46211  vonioolem2  46239  vonioo  46240  vonicclem2  46242  vonicc  46243  smfid  46310  smflimlem3  46331  natglobalincr  46433  tworepnotupword  46442  2elfz2melfz  46868  smonoord  46880  iccpart  46925  iccpartimp  46926  iccpartres  46927  sqrtpwpw2p  47047  grlicsym  47440  grlictr  47442  ismgmALT  47537  iscmgmALT  47538  issgrpALT  47539  iscsgrpALT  47540  lindslinindsimp2lem5  47782  rrx2plordisom  48048  aacllem  48486