Theorem breq12d 5179

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  breq123d  5180  3brtr3d  5197  3brtr4d  5198  sbcbr  5221  pocl  5615  poclOLD  5616  csbcnvgALT  5909  cnvpo  6318  sbcfung  6602  isoeq1  7353  isocnv  7366  isotr  7372  caovordig  7655  caovordg  7657  caovord2d  7659  caovord  7661  ofrfvalg  7722  ofrval  7726  ofrfval2  7735  caofref  7744  fnwelem  8172  poseq  8199  fundmeng  9097  enrefnn  9113  xpsneng  9122  xpcomeng  9130  xpdom2g  9134  limensuc  9220  infensuc  9221  pssnn  9234  unxpdom  9316  dif1ennnALT  9339  unfilem3  9373  fodomfi  9378  domunfican  9389  fodomfiOLD  9398  marypha1lem  9502  infsupprpr  9573  wemaplem1  9615  wemaplem2  9616  wemapwe  9766  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  dmttrcl  9790  rnttrcl  9791  ttrclselem2  9795  dif1card  10079  infxpenlem  10082  nnadju  10267  pwsdompw  10272  infmap2  10286  sornom  10346  isfin5  10368  isfin6  10369  domtriomlem  10511  axdc2lem  10517  axdclem2  10589  pwcfsdom  10652  cfpwsdom  10653  alephom  10654  fpwwe2lem6  10705  fpwwe2lem8  10707  tskcard  10850  ordpipq  11011  adderpqlem  11023  mulerpqlem  11024  mulcanenq  11029  lterpq  11039  ltanq  11040  ltmnq  11041  ltaddnq  11043  ltrnq  11048  archnq  11049  reclem4pr  11119  ltasr  11169  sqgt0sr  11175  axpre-ltadd  11236  axpre-mulgt0  11237  ltadd1  11757  leadd2  11759  ltmul2  12145  lemul2  12147  lemul1a  12148  ltdiv1  12159  ltdiv2  12181  lediv2  12185  div4p1lem1div2  12548  nn0ledivnn  13170  xleadd1  13317  xltadd2  13319  xsubge0  13323  xlemul1a  13350  xlemul1  13352  xlemul2  13353  xltmul2  13355  ltdifltdiv  13885  fzennn  14019  monoord  14083  monoord2  14084  expmordi  14217  ltexp2r  14223  leexp1a  14225  sqlecan  14258  bernneq  14278  faclbnd  14339  faclbnd3  14341  faclbnd4lem1  14342  faclbnd4lem2  14343  faclbnd4lem3  14344  faclbnd4lem4  14345  faclbnd6  14348  facubnd  14349  rlimcld2  15624  isercoll2  15717  climsup  15718  iseraltlem2  15731  fsumabs  15849  fsumrlim  15859  climcndslem1  15897  climcndslem2  15898  supcvg  15904  geomulcvg  15924  cvgrat  15931  ntrivcvgtail  15948  ruclem2  16280  ruclem8  16285  addmodlteqALT  16373  fproddvdsd  16383  sadcaddlem  16503  sadcadd  16504  nn0seqcvgd  16617  algcvg  16623  algcvga  16626  eucalgcvga  16633  isprm5  16754  qnumgt0  16797  pcprendvds2  16888  pcpremul  16890  pcadd2  16937  prmreclem4  16966  prmreclem5  16967  prmreclem6  16968  2expltfac  17140  xpsle  17639  mreexexlemd  17702  issubc  17899  latjlej2  18524  latmlem2  18540  sylow1lem3  19642  isslw  19650  fislw  19667  efgi  19761  lt6abl  19937  ablfac1eu  20117  isabv  20834  abvtri  20845  psdmul  22193  cayleyhamilton1  22919  isucn  24308  ispsmet  24335  psmettri2  24340  ismet  24354  isxmet  24355  xmettri2  24371  imasdsf1olem  24404  imasf1oxmet  24406  blvalps  24416  blval  24417  comet  24547  stdbdxmet  24549  nrmmetd  24608  tngngp  24696  tngngp3  24698  nmofval  24756  nmolb2d  24760  nmoi  24770  nmoix  24771  icopnfhmeo  24993  xrhmeo  24996  evth2  25011  pi1grplem  25101  minveclem6  25487  ovolfiniun  25555  ovoliunlem3  25558  voliunlem3  25606  ioombl1  25616  mbfmax  25703  mbfpos  25705  itg1climres  25769  mbfi1fseqlem2  25771  mbfi1fseqlem6  25775  mbfi1fseq  25776  mbfmullem  25780  itg2split  25804  itg2monolem1  25805  itg2monolem3  25807  itg2mono  25808  itg2i1fseqle  25809  itg2i1fseq  25810  itg2i1fseq2  25811  itg2addlem  25813  rolle  26048  dvlip  26052  c1lip1  26056  dvcnvrelem1  26076  dvcvx  26079  ply1divex  26196  q1pval  26214  fta1glem2  26228  fta1g  26229  fta1b  26231  plydivlem3  26355  fta1lem  26367  fta1  26368  aalioulem3  26394  aalioulem4  26395  aaliou3lem2  26403  aaliou3lem8  26405  aaliou3lem9  26410  ulmdvlem1  26461  ulmdvlem3  26463  abelthlem2  26494  abelthlem7a  26499  argrege0  26671  cxplt  26754  cxplea  26756  cxple2  26757  cxplt3  26760  logbleb  26844  logblt  26845  rlimcxp  27035  scvxcvx  27047  jensenlem2  27049  ftalem3  27136  ftalem7  27140  vmalelog  27267  chtub  27274  chpchtsum  27281  bclbnd  27342  efexple  27343  bposlem5  27350  bposlem6  27351  bposlem7  27352  lgsdilem  27386  2lgslem1a2  27452  2sqreuop  27524  2sqreuopnn  27525  2sqreuoplt  27526  2sqreuopltb  27527  2sqreuopnnlt  27528  2sqreuopnnltb  27529  dchrisumlem3  27553  dchrmusumlema  27555  dchrmusum2  27556  dchrvmasumlem2  27560  dchrvmasumlema  27562  dchrvmasumiflem1  27563  dchrisum0flblem2  27571  dchrisum0flb  27572  dchrisum0lema  27576  dchrisum0lem1b  27577  dchrisum0lem2  27580  pntrlog2bndlem2  27640  pntibndlem2  27653  pntlemf  27667  ostth2lem1  27680  qabvle  27687  sltval2  27719  sltres  27725  nolesgn2o  27734  nogesgn1o  27736  nodense  27755  nolt02o  27758  nogt01o  27759  noresle  27760  nosupbnd2lem1  27778  nosupbnd2  27779  noinfbnd2lem1  27793  noinfbnd2  27794  addsproplem1  28020  addsprop  28027  sltadd2im  28037  sleadd2im  28039  sleadd1  28040  sleadd2  28041  sltadd1  28043  sltsub1  28124  sltsub2  28125  sltsubsubbd  28131  sltsubsub2bd  28132  posdifsd  28145  subsge0d  28147  mulsproplemcbv  28159  mulsproplem1  28160  mulsprop  28174  slemuld  28182  sltmul1d  28217  sltmulneg1d  28220  sltmulneg2d  28221  slemul1ad  28226  legso  28625  iscgra  28835  isleag  28873  iseqlg  28893  brbtwn2  28938  axlowdim  28994  ewlksfval  29637  isnvlem  30642  nvtri  30702  nmlnoubi  30828  nmblolbii  30831  nmblolbi  30832  blocnilem  30836  sii  30886  ubthlem2  30903  minvecolem3  30908  minvecolem5  30913  minvecolem6  30914  norm-ii  31170  norm3dif  31182  norm3adifi  31185  bcs  31213  pjnorm  31756  pjnel  31758  nmbdoplbi  32056  nmbdoplb  32057  nmcoplb  32062  lnconi  32065  nmbdfnlb  32082  nmcfnlb  32086  pjdifnormi  32199  mdslmd2i  32362  cvmd  32368  cvexch  32406  cdj1i  32465  cdj3lem1  32466  cdj3lem2b  32469  cdj3lem3b  32472  cdj3i  32473  isoun  32713  ismnt  32956  mgcmntco  32967  dfmgc2lem  32968  dfmgc2  32969  mgcf1o  32976  ischn  32979  chnltm1  32981  chnind  32983  chnub  32984  isomnd  33051  omndadd  33056  omndmul  33064  ogrpinvlt  33073  gsumle  33074  isinftm  33161  rlocaddval  33240  rlocmulval  33241  fldext2chn  33719  xrmulc1cn  33876  lmdvg  33899  nexple  33973  faeval  34210  brfae  34212  inelcarsg  34276  carsgsigalem  34280  carsgclctunlem2  34284  carsgclctun  34286  hgt750lemc  34624  hgt750lemd  34625  hgt749d  34626  sconnpht  35197  snmlval  35299  satfv1lem  35330  satfv1  35331  satfv0fun  35339  satfv0fvfmla0  35381  lediv2aALT  35645  faclim  35708  fvtransport  35996  idinside  36048  btwnconn1lem7  36057  btwnconn1lem11  36061  btwnconn1lem12  36062  ditgeq123dv  36187  cbvditgdavw2  36264  nn0prpwlem  36288  weiunlem1  36428  weiunfrlem  36430  bj-opabco  37154  poimirlem29  37609  heicant  37615  itg2addnclem  37631  itg2addnclem3  37633  itg2gt0cn  37635  ftc1anclem6  37658  ftc1anc  37661  ftc2nc  37662  dvasin  37664  areacirclem1  37668  seqpo  37707  incsequz  37708  metf1o  37715  mettrifi  37717  cntotbnd  37756  heiborlem4  37774  heiborlem6  37776  heiborlem10  37780  bfplem1  37782  bfplem2  37783  isopos  39136  oplecon3b  39156  atlatle  39276  4at2  39571  pmaple  39718  islaut  40040  lautcnvle  40046  lautco  40054  ltrncnvel  40099  cdlemeg49lebilem  40496  cdlemg17h  40625  tendoset  40716  tendotp  40718  cdlemk39s  40896  lcmineqlem23  42008  lcmineqlem  42009  intlewftc  42018  aks4d1p1p4  42028  dvle2  42029  aks4d1p8d2  42042  aks4d1p9  42045  aks4d1  42046  2ap1caineq  42102  sticksstones1  42103  sticksstones2  42104  sticksstones3  42105  sticksstones8  42110  sticksstones10  42112  sticksstones11  42113  sticksstones12a  42114  sticksstones15  42118  aks6d1c7lem3  42139  unitscyglem1  42152  factwoffsmonot  42199  brif12  42218  dvdsexpnn0  42321  dvdsexpb  42322  reltsub1  42362  irrapxlem2  42779  irrapxlem4  42781  irrapxlem5  42782  irrapxlem6  42783  pellexlem3  42787  monotuz  42898  monotoddzzfi  42899  monotoddzz  42900  jm2.17a  42917  jm2.17b  42918  rmygeid  42921  rmydioph  42971  expdiophlem1  42978  expdiophlem2  42979  ttac  42993  fnwe2lem2  43008  relexp01min  43675  cvgdvgrat  44282  monoords  45212  supxrgelem  45252  supxrge  45253  abslt2sqd  45275  ltmulneg  45307  ltdiv23neg  45309  monoordxrv  45397  monoordxr  45398  monoord2xrv  45399  monoord2xr  45400  evthiccabs  45414  sqrlearg  45471  climinf  45527  climinff  45532  limsupres  45626  climinf2  45628  climinf2mpt  45635  climinfmpt  45636  supcnvlimsup  45661  liminfval2  45689  liminflelimsuplem  45696  liminfltlem  45725  fprodsubrecnncnvlem  45828  fprodaddrecnncnvlem  45830  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  iblspltprt  45894  itgspltprt  45900  stoweidlem3  45924  fourierdlem2  46030  fourierdlem3  46031  fourierdlem11  46039  fourierdlem12  46040  fourierdlem15  46043  fourierdlem34  46062  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem79  46106  fourierdlem83  46110  fourierdlem89  46116  fourierdlem91  46118  fourierdlem100  46127  fourierdlem107  46134  fourierdlem109  46136  fourierdlem112  46139  etransclem31  46186  etransclem32  46187  rrndistlt  46211  ioorrnopn  46226  ioorrnopnxrlem  46227  sge0less  46313  sge0le  46328  sge0split  46330  sge0lempt  46331  sge0iunmptlemre  46336  sge0isum  46348  sge0seq  46367  meaiuninclem  46401  meaiininclem  46407  meaiininc  46408  isome  46415  omeunile  46426  omeiunlempt  46441  carageniuncllem2  46443  0ome  46450  isomenndlem  46451  isomennd  46452  ovnssle  46482  ovnsubadd  46493  hsphoidmvle2  46506  hsphoidmvle  46507  hoidmvval0  46508  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoidmvlelem5  46520  hoidmvle  46521  hoidifhspdmvle  46541  hspmbllem2  46548  hspmbl  46550  ovnsubadd2lem  46566  ovolval4lem2  46571  ovolval4  46572  ovolval5lem2  46574  vonioolem2  46602  vonioo  46603  vonicclem2  46605  vonicc  46606  smfid  46673  smflimlem3  46694  natglobalincr  46796  tworepnotupword  46805  2elfz2melfz  47233  smonoord  47245  iccpart  47290  iccpartimp  47291  iccpartres  47292  sqrtpwpw2p  47412  grlicsym  47830  grlictr  47832  ismgmALT  47946  iscmgmALT  47947  issgrpALT  47948  iscsgrpALT  47949  lindslinindsimp2lem5  48191  rrx2plordisom  48457  aacllem  48895