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  27455  addsprop  27462  sltadd2im  27472  sleadd2im  27474  sleadd1  27475  sleadd2  27476  sltadd1  27478  sltsub1  27546  sltsub2  27547  sltsubsubbd  27553  sltsubsub2bd  27554  posdifsd  27564  mulsproplemcbv  27574  mulsproplem1  27575  mulsprop  27589  slemuld  27597  sltmul1d  27628  sltmulneg1d  27631  sltmulneg2d  27632  legso  27881  iscgra  28091  isleag  28129  iseqlg  28149  brbtwn2  28194  axlowdim  28250  ewlksfval  28889  isnvlem  29894  nvtri  29954  nmlnoubi  30080  nmblolbii  30083  nmblolbi  30084  blocnilem  30088  sii  30138  ubthlem2  30155  minvecolem3  30160  minvecolem5  30165  minvecolem6  30166  norm-ii  30422  norm3dif  30434  norm3adifi  30437  bcs  30465  pjnorm  31008  pjnel  31010  nmbdoplbi  31308  nmbdoplb  31309  nmcoplb  31314  lnconi  31317  nmbdfnlb  31334  nmcfnlb  31338  pjdifnormi  31451  mdslmd2i  31614  cvmd  31620  cvexch  31658  cdj1i  31717  cdj3lem1  31718  cdj3lem2b  31721  cdj3lem3b  31724  cdj3i  31725  isoun  31954  ismnt  32184  mgcmntco  32195  dfmgc2lem  32196  dfmgc2  32197  mgcf1o  32204  isomnd  32250  omndadd  32255  omndmul  32263  ogrpinvlt  32272  gsumle  32273  isinftm  32358  xrmulc1cn  32941  lmdvg  32964  nexple  33038  faeval  33275  brfae  33277  inelcarsg  33341  carsgsigalem  33345  carsgclctunlem2  33349  carsgclctun  33351  hgt750lemc  33690  hgt750lemd  33691  hgt749d  33692  sconnpht  34251  snmlval  34353  satfv1lem  34384  satfv1  34385  satfv0fun  34393  satfv0fvfmla0  34435  lediv2aALT  34693  faclim  34747  fvtransport  35035  idinside  35087  btwnconn1lem7  35096  btwnconn1lem11  35100  btwnconn1lem12  35101  nn0prpwlem  35255  bj-opabco  36117  poimirlem29  36565  heicant  36571  itg2addnclem  36587  itg2addnclem3  36589  itg2gt0cn  36591  ftc1anclem6  36614  ftc1anc  36617  ftc2nc  36618  dvasin  36620  areacirclem1  36624  seqpo  36663  incsequz  36664  metf1o  36671  mettrifi  36673  cntotbnd  36712  heiborlem4  36730  heiborlem6  36732  heiborlem10  36736  bfplem1  36738  bfplem2  36739  isopos  38098  oplecon3b  38118  atlatle  38238  4at2  38533  pmaple  38680  islaut  39002  lautcnvle  39008  lautco  39016  ltrncnvel  39061  cdlemeg49lebilem  39458  cdlemg17h  39587  tendoset  39678  tendotp  39680  cdlemk39s  39858  lcmineqlem23  40964  lcmineqlem  40965  intlewftc  40974  aks4d1p1p4  40984  dvle2  40985  aks4d1p8d2  40998  aks4d1p9  41001  aks4d1  41002  2ap1caineq  41009  sticksstones1  41010  sticksstones2  41011  sticksstones3  41012  sticksstones8  41017  sticksstones10  41019  sticksstones11  41020  sticksstones12a  41021  sticksstones15  41025  factwoffsmonot  41071  brif12  41091  dvdsexpnn0  41280  dvdsexpb  41281  reltsub1  41307  irrapxlem2  41609  irrapxlem4  41611  irrapxlem5  41612  irrapxlem6  41613  pellexlem3  41617  monotuz  41728  monotoddzzfi  41729  monotoddzz  41730  jm2.17a  41747  jm2.17b  41748  rmygeid  41751  rmydioph  41801  expdiophlem1  41808  expdiophlem2  41809  ttac  41823  fnwe2lem2  41841  relexp01min  42512  cvgdvgrat  43120  monoords  44055  supxrgelem  44095  supxrge  44096  abslt2sqd  44118  ltmulneg  44150  ltdiv23neg  44152  monoordxrv  44240  monoordxr  44241  monoord2xrv  44242  monoord2xr  44243  evthiccabs  44257  sqrlearg  44314  climinf  44370  climinff  44375  limsupres  44469  climinf2  44471  climinf2mpt  44478  climinfmpt  44479  supcnvlimsup  44504  liminfval2  44532  liminflelimsuplem  44539  liminfltlem  44568  fprodsubrecnncnvlem  44671  fprodaddrecnncnvlem  44673  ioodvbdlimc1lem1  44695  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  iblspltprt  44737  itgspltprt  44743  stoweidlem3  44767  fourierdlem2  44873  fourierdlem3  44874  fourierdlem11  44882  fourierdlem12  44883  fourierdlem15  44886  fourierdlem34  44905  fourierdlem41  44912  fourierdlem48  44918  fourierdlem49  44919  fourierdlem79  44949  fourierdlem83  44953  fourierdlem89  44959  fourierdlem91  44961  fourierdlem100  44970  fourierdlem107  44977  fourierdlem109  44979  fourierdlem112  44982  etransclem31  45029  etransclem32  45030  rrndistlt  45054  ioorrnopn  45069  ioorrnopnxrlem  45070  sge0less  45156  sge0le  45171  sge0split  45173  sge0lempt  45174  sge0iunmptlemre  45179  sge0isum  45191  sge0seq  45210  meaiuninclem  45244  meaiininclem  45250  meaiininc  45251  isome  45258  omeunile  45269  omeiunlempt  45284  carageniuncllem2  45286  0ome  45293  isomenndlem  45294  isomennd  45295  ovnssle  45325  ovnsubadd  45336  hsphoidmvle2  45349  hsphoidmvle  45350  hoidmvval0  45351  hoidmv1lelem1  45355  hoidmv1lelem2  45356  hoidmv1lelem3  45357  hoidmv1le  45358  hoidmvlelem1  45359  hoidmvlelem2  45360  hoidmvlelem3  45361  hoidmvlelem4  45362  hoidmvlelem5  45363  hoidmvle  45364  hoidifhspdmvle  45384  hspmbllem2  45391  hspmbl  45393  ovnsubadd2lem  45409  ovolval4lem2  45414  ovolval4  45415  ovolval5lem2  45417  vonioolem2  45445  vonioo  45446  vonicclem2  45448  vonicc  45449  smfid  45516  smflimlem3  45537  natglobalincr  45639  tworepnotupword  45648  2elfz2melfz  46074  smonoord  46087  iccpart  46132  iccpartimp  46133  iccpartres  46134  sqrtpwpw2p  46254  ismgmALT  46681  iscmgmALT  46682  issgrpALT  46683  iscsgrpALT  46684  lindslinindsimp2lem5  47191  rrx2plordisom  47457  aacllem  47896