Theorem breq12d 5162

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  breq123d  5163  3brtr3d  5180  3brtr4d  5181  sbcbr  5204  pocl  5596  poclOLD  5597  csbcnvgALT  5885  cnvpo  6287  sbcfung  6573  isoeq1  7314  isocnv  7327  isotr  7333  caovordig  7612  caovordg  7614  caovord2d  7616  caovord  7618  ofrfvalg  7678  ofrval  7682  ofrfval2  7691  caofref  7699  fnwelem  8117  poseq  8144  fundmeng  9032  enrefnn  9047  xpsneng  9056  xpcomeng  9064  xpdom2g  9068  limensuc  9154  infensuc  9155  pssnn  9168  unxpdom  9253  pssnnOLD  9265  dif1ennnALT  9277  unfilem3  9312  unfiOLD  9313  domunfican  9320  fodomfi  9325  marypha1lem  9428  infsupprpr  9499  wemaplem1  9541  wemaplem2  9542  wemapwe  9692  ssttrcl  9710  ttrcltr  9711  ttrclss  9715  dmttrcl  9716  rnttrcl  9717  ttrclselem2  9721  dif1card  10005  infxpenlem  10008  nnadju  10192  pwsdompw  10199  infmap2  10213  sornom  10272  isfin5  10294  isfin6  10295  domtriomlem  10437  axdc2lem  10443  axdclem2  10515  pwcfsdom  10578  cfpwsdom  10579  alephom  10580  fpwwe2lem6  10631  fpwwe2lem8  10633  tskcard  10776  ordpipq  10937  adderpqlem  10949  mulerpqlem  10950  mulcanenq  10955  lterpq  10965  ltanq  10966  ltmnq  10967  ltaddnq  10969  ltrnq  10974  archnq  10975  reclem4pr  11045  ltasr  11095  sqgt0sr  11101  axpre-ltadd  11162  axpre-mulgt0  11163  ltadd1  11681  leadd2  11683  ltmul2  12065  lemul2  12067  lemul1a  12068  ltdiv1  12078  ltdiv2  12100  lediv2  12104  div4p1lem1div2  12467  nn0ledivnn  13087  xleadd1  13234  xltadd2  13236  xsubge0  13240  xlemul1a  13267  xlemul1  13269  xlemul2  13270  xltmul2  13272  ltdifltdiv  13799  fzennn  13933  monoord  13998  monoord2  13999  expmordi  14132  ltexp2r  14138  leexp1a  14140  sqlecan  14173  bernneq  14192  faclbnd  14250  faclbnd3  14252  faclbnd4lem1  14253  faclbnd4lem2  14254  faclbnd4lem3  14255  faclbnd4lem4  14256  faclbnd6  14259  facubnd  14260  rlimcld2  15522  isercoll2  15615  climsup  15616  iseraltlem2  15629  fsumabs  15747  fsumrlim  15757  climcndslem1  15795  climcndslem2  15796  supcvg  15802  geomulcvg  15822  cvgrat  15829  ntrivcvgtail  15846  ruclem2  16175  ruclem8  16180  addmodlteqALT  16268  fproddvdsd  16278  sadcaddlem  16398  sadcadd  16399  nn0seqcvgd  16507  algcvg  16513  algcvga  16516  eucalgcvga  16523  isprm5  16644  qnumgt0  16686  pcprendvds2  16774  pcpremul  16776  pcadd2  16823  prmreclem4  16852  prmreclem5  16853  prmreclem6  16854  2expltfac  17026  xpsle  17525  mreexexlemd  17588  issubc  17785  latjlej2  18407  latmlem2  18423  sylow1lem3  19468  isslw  19476  fislw  19493  efgi  19587  lt6abl  19763  ablfac1eu  19943  isabv  20427  abvtri  20438  cayleyhamilton1  22394  isucn  23783  ispsmet  23810  psmettri2  23815  ismet  23829  isxmet  23830  xmettri2  23846  imasdsf1olem  23879  imasf1oxmet  23881  blvalps  23891  blval  23892  comet  24022  stdbdxmet  24024  nrmmetd  24083  tngngp  24171  tngngp3  24173  nmofval  24231  nmolb2d  24235  nmoi  24245  nmoix  24246  icopnfhmeo  24459  xrhmeo  24462  evth2  24476  pi1grplem  24565  minveclem6  24951  ovolfiniun  25018  ovoliunlem3  25021  voliunlem3  25069  ioombl1  25079  mbfmax  25166  mbfpos  25168  itg1climres  25232  mbfi1fseqlem2  25234  mbfi1fseqlem6  25238  mbfi1fseq  25239  mbfmullem  25243  itg2split  25267  itg2monolem1  25268  itg2monolem3  25270  itg2mono  25271  itg2i1fseqle  25272  itg2i1fseq  25273  itg2i1fseq2  25274  itg2addlem  25276  rolle  25507  dvlip  25510  c1lip1  25514  dvcnvrelem1  25534  dvcvx  25537  ply1divex  25654  q1pval  25671  fta1glem2  25684  fta1g  25685  fta1b  25687  plydivlem3  25808  fta1lem  25820  fta1  25821  aalioulem3  25847  aalioulem4  25848  aaliou3lem2  25856  aaliou3lem8  25858  aaliou3lem9  25863  ulmdvlem1  25912  ulmdvlem3  25914  abelthlem2  25944  abelthlem7a  25949  argrege0  26119  cxplt  26202  cxplea  26204  cxple2  26205  cxplt3  26208  logbleb  26288  logblt  26289  rlimcxp  26478  scvxcvx  26490  jensenlem2  26492  ftalem3  26579  ftalem7  26583  vmalelog  26708  chtub  26715  chpchtsum  26722  bclbnd  26783  efexple  26784  bposlem5  26791  bposlem6  26792  bposlem7  26793  lgsdilem  26827  2lgslem1a2  26893  2sqreuop  26965  2sqreuopnn  26966  2sqreuoplt  26967  2sqreuopltb  26968  2sqreuopnnlt  26969  2sqreuopnnltb  26970  dchrisumlem3  26994  dchrmusumlema  26996  dchrmusum2  26997  dchrvmasumlem2  27001  dchrvmasumlema  27003  dchrvmasumiflem1  27004  dchrisum0flblem2  27012  dchrisum0flb  27013  dchrisum0lema  27017  dchrisum0lem1b  27018  dchrisum0lem2  27021  pntrlog2bndlem2  27081  pntibndlem2  27094  pntlemf  27108  ostth2lem1  27121  qabvle  27128  sltval2  27159  sltres  27165  nolesgn2o  27174  nogesgn1o  27176  nodense  27195  nolt02o  27198  nogt01o  27199  noresle  27200  nosupbnd2lem1  27218  nosupbnd2  27219  noinfbnd2lem1  27233  noinfbnd2  27234  addsproplem1  27453  addsprop  27460  sltadd2im  27469  sleadd2im  27471  sleadd1  27472  sleadd2  27473  sltadd1  27475  sltsub1  27543  sltsub2  27544  sltsubsubbd  27550  sltsubsub2bd  27551  posdifsd  27561  mulsproplemcbv  27571  mulsproplem1  27572  mulsprop  27586  slemuld  27594  sltmul1d  27625  sltmulneg1d  27628  sltmulneg2d  27629  legso  27850  iscgra  28060  isleag  28098  iseqlg  28118  brbtwn2  28163  axlowdim  28219  ewlksfval  28858  isnvlem  29863  nvtri  29923  nmlnoubi  30049  nmblolbii  30052  nmblolbi  30053  blocnilem  30057  sii  30107  ubthlem2  30124  minvecolem3  30129  minvecolem5  30134  minvecolem6  30135  norm-ii  30391  norm3dif  30403  norm3adifi  30406  bcs  30434  pjnorm  30977  pjnel  30979  nmbdoplbi  31277  nmbdoplb  31278  nmcoplb  31283  lnconi  31286  nmbdfnlb  31303  nmcfnlb  31307  pjdifnormi  31420  mdslmd2i  31583  cvmd  31589  cvexch  31627  cdj1i  31686  cdj3lem1  31687  cdj3lem2b  31690  cdj3lem3b  31693  cdj3i  31694  isoun  31923  ismnt  32153  mgcmntco  32164  dfmgc2lem  32165  dfmgc2  32166  mgcf1o  32173  isomnd  32219  omndadd  32224  omndmul  32232  ogrpinvlt  32241  gsumle  32242  isinftm  32327  xrmulc1cn  32910  lmdvg  32933  nexple  33007  faeval  33244  brfae  33246  inelcarsg  33310  carsgsigalem  33314  carsgclctunlem2  33318  carsgclctun  33320  hgt750lemc  33659  hgt750lemd  33660  hgt749d  33661  sconnpht  34220  snmlval  34322  satfv1lem  34353  satfv1  34354  satfv0fun  34362  satfv0fvfmla0  34404  lediv2aALT  34662  faclim  34716  fvtransport  35004  idinside  35056  btwnconn1lem7  35065  btwnconn1lem11  35069  btwnconn1lem12  35070  nn0prpwlem  35207  bj-opabco  36069  poimirlem29  36517  heicant  36523  itg2addnclem  36539  itg2addnclem3  36541  itg2gt0cn  36543  ftc1anclem6  36566  ftc1anc  36569  ftc2nc  36570  dvasin  36572  areacirclem1  36576  seqpo  36615  incsequz  36616  metf1o  36623  mettrifi  36625  cntotbnd  36664  heiborlem4  36682  heiborlem6  36684  heiborlem10  36688  bfplem1  36690  bfplem2  36691  isopos  38050  oplecon3b  38070  atlatle  38190  4at2  38485  pmaple  38632  islaut  38954  lautcnvle  38960  lautco  38968  ltrncnvel  39013  cdlemeg49lebilem  39410  cdlemg17h  39539  tendoset  39630  tendotp  39632  cdlemk39s  39810  lcmineqlem23  40916  lcmineqlem  40917  intlewftc  40926  aks4d1p1p4  40936  dvle2  40937  aks4d1p8d2  40950  aks4d1p9  40953  aks4d1  40954  2ap1caineq  40961  sticksstones1  40962  sticksstones2  40963  sticksstones3  40964  sticksstones8  40969  sticksstones10  40971  sticksstones11  40972  sticksstones12a  40973  sticksstones15  40977  factwoffsmonot  41023  brif12  41043  dvdsexpnn0  41232  dvdsexpb  41233  reltsub1  41259  irrapxlem2  41561  irrapxlem4  41563  irrapxlem5  41564  irrapxlem6  41565  pellexlem3  41569  monotuz  41680  monotoddzzfi  41681  monotoddzz  41682  jm2.17a  41699  jm2.17b  41700  rmygeid  41703  rmydioph  41753  expdiophlem1  41760  expdiophlem2  41761  ttac  41775  fnwe2lem2  41793  relexp01min  42464  cvgdvgrat  43072  monoords  44007  supxrgelem  44047  supxrge  44048  abslt2sqd  44070  ltmulneg  44102  ltdiv23neg  44104  monoordxrv  44192  monoordxr  44193  monoord2xrv  44194  monoord2xr  44195  evthiccabs  44209  sqrlearg  44266  climinf  44322  climinff  44327  limsupres  44421  climinf2  44423  climinf2mpt  44430  climinfmpt  44431  supcnvlimsup  44456  liminfval2  44484  liminflelimsuplem  44491  liminfltlem  44520  fprodsubrecnncnvlem  44623  fprodaddrecnncnvlem  44625  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  iblspltprt  44689  itgspltprt  44695  stoweidlem3  44719  fourierdlem2  44825  fourierdlem3  44826  fourierdlem11  44834  fourierdlem12  44835  fourierdlem15  44838  fourierdlem34  44857  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  fourierdlem79  44901  fourierdlem83  44905  fourierdlem89  44911  fourierdlem91  44913  fourierdlem100  44922  fourierdlem107  44929  fourierdlem109  44931  fourierdlem112  44934  etransclem31  44981  etransclem32  44982  rrndistlt  45006  ioorrnopn  45021  ioorrnopnxrlem  45022  sge0less  45108  sge0le  45123  sge0split  45125  sge0lempt  45126  sge0iunmptlemre  45131  sge0isum  45143  sge0seq  45162  meaiuninclem  45196  meaiininclem  45202  meaiininc  45203  isome  45210  omeunile  45221  omeiunlempt  45236  carageniuncllem2  45238  0ome  45245  isomenndlem  45246  isomennd  45247  ovnssle  45277  ovnsubadd  45288  hsphoidmvle2  45301  hsphoidmvle  45302  hoidmvval0  45303  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmv1lelem3  45309  hoidmv1le  45310  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  hoidmvlelem5  45315  hoidmvle  45316  hoidifhspdmvle  45336  hspmbllem2  45343  hspmbl  45345  ovnsubadd2lem  45361  ovolval4lem2  45366  ovolval4  45367  ovolval5lem2  45369  vonioolem2  45397  vonioo  45398  vonicclem2  45400  vonicc  45401  smfid  45468  smflimlem3  45489  natglobalincr  45591  tworepnotupword  45600  2elfz2melfz  46026  smonoord  46039  iccpart  46084  iccpartimp  46085  iccpartres  46086  sqrtpwpw2p  46206  ismgmALT  46633  iscmgmALT  46634  issgrpALT  46635  iscsgrpALT  46636  lindslinindsimp2lem5  47143  rrx2plordisom  47409  aacllem  47848