Theorem breq12d 5161

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

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

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  breq123d  5162  3brtr3d  5179  3brtr4d  5180  sbcbr  5203  pocl  5595  poclOLD  5596  csbcnvgALT  5883  cnvpo  6284  sbcfung  6570  isoeq1  7311  isocnv  7324  isotr  7330  caovordig  7609  caovordg  7611  caovord2d  7613  caovord  7615  ofrfvalg  7675  ofrval  7679  ofrfval2  7688  caofref  7696  fnwelem  8114  poseq  8141  fundmeng  9029  enrefnn  9044  xpsneng  9053  xpcomeng  9061  xpdom2g  9065  limensuc  9151  infensuc  9152  pssnn  9165  unxpdom  9250  pssnnOLD  9262  dif1ennnALT  9274  unfilem3  9309  unfiOLD  9310  domunfican  9317  fodomfi  9322  marypha1lem  9425  infsupprpr  9496  wemaplem1  9538  wemaplem2  9539  wemapwe  9689  ssttrcl  9707  ttrcltr  9708  ttrclss  9712  dmttrcl  9713  rnttrcl  9714  ttrclselem2  9718  dif1card  10002  infxpenlem  10005  nnadju  10189  pwsdompw  10196  infmap2  10210  sornom  10269  isfin5  10291  isfin6  10292  domtriomlem  10434  axdc2lem  10440  axdclem2  10512  pwcfsdom  10575  cfpwsdom  10576  alephom  10577  fpwwe2lem6  10628  fpwwe2lem8  10630  tskcard  10773  ordpipq  10934  adderpqlem  10946  mulerpqlem  10947  mulcanenq  10952  lterpq  10962  ltanq  10963  ltmnq  10964  ltaddnq  10966  ltrnq  10971  archnq  10972  reclem4pr  11042  ltasr  11092  sqgt0sr  11098  axpre-ltadd  11159  axpre-mulgt0  11160  ltadd1  11678  leadd2  11680  ltmul2  12062  lemul2  12064  lemul1a  12065  ltdiv1  12075  ltdiv2  12097  lediv2  12101  div4p1lem1div2  12464  nn0ledivnn  13084  xleadd1  13231  xltadd2  13233  xsubge0  13237  xlemul1a  13264  xlemul1  13266  xlemul2  13267  xltmul2  13269  ltdifltdiv  13796  fzennn  13930  monoord  13995  monoord2  13996  expmordi  14129  ltexp2r  14135  leexp1a  14137  sqlecan  14170  bernneq  14189  faclbnd  14247  faclbnd3  14249  faclbnd4lem1  14250  faclbnd4lem2  14251  faclbnd4lem3  14252  faclbnd4lem4  14253  faclbnd6  14256  facubnd  14257  rlimcld2  15519  isercoll2  15612  climsup  15613  iseraltlem2  15626  fsumabs  15744  fsumrlim  15754  climcndslem1  15792  climcndslem2  15793  supcvg  15799  geomulcvg  15819  cvgrat  15826  ntrivcvgtail  15843  ruclem2  16172  ruclem8  16177  addmodlteqALT  16265  fproddvdsd  16275  sadcaddlem  16395  sadcadd  16396  nn0seqcvgd  16504  algcvg  16510  algcvga  16513  eucalgcvga  16520  isprm5  16641  qnumgt0  16683  pcprendvds2  16771  pcpremul  16773  pcadd2  16820  prmreclem4  16849  prmreclem5  16850  prmreclem6  16851  2expltfac  17023  xpsle  17522  mreexexlemd  17585  issubc  17782  latjlej2  18404  latmlem2  18420  sylow1lem3  19463  isslw  19471  fislw  19488  efgi  19582  lt6abl  19758  ablfac1eu  19938  isabv  20420  abvtri  20431  cayleyhamilton1  22386  isucn  23775  ispsmet  23802  psmettri2  23807  ismet  23821  isxmet  23822  xmettri2  23838  imasdsf1olem  23871  imasf1oxmet  23873  blvalps  23883  blval  23884  comet  24014  stdbdxmet  24016  nrmmetd  24075  tngngp  24163  tngngp3  24165  nmofval  24223  nmolb2d  24227  nmoi  24237  nmoix  24238  icopnfhmeo  24451  xrhmeo  24454  evth2  24468  pi1grplem  24557  minveclem6  24943  ovolfiniun  25010  ovoliunlem3  25013  voliunlem3  25061  ioombl1  25071  mbfmax  25158  mbfpos  25160  itg1climres  25224  mbfi1fseqlem2  25226  mbfi1fseqlem6  25230  mbfi1fseq  25231  mbfmullem  25235  itg2split  25259  itg2monolem1  25260  itg2monolem3  25262  itg2mono  25263  itg2i1fseqle  25264  itg2i1fseq  25265  itg2i1fseq2  25266  itg2addlem  25268  rolle  25499  dvlip  25502  c1lip1  25506  dvcnvrelem1  25526  dvcvx  25529  ply1divex  25646  q1pval  25663  fta1glem2  25676  fta1g  25677  fta1b  25679  plydivlem3  25800  fta1lem  25812  fta1  25813  aalioulem3  25839  aalioulem4  25840  aaliou3lem2  25848  aaliou3lem8  25850  aaliou3lem9  25855  ulmdvlem1  25904  ulmdvlem3  25906  abelthlem2  25936  abelthlem7a  25941  argrege0  26111  cxplt  26194  cxplea  26196  cxple2  26197  cxplt3  26200  logbleb  26278  logblt  26279  rlimcxp  26468  scvxcvx  26480  jensenlem2  26482  ftalem3  26569  ftalem7  26573  vmalelog  26698  chtub  26705  chpchtsum  26712  bclbnd  26773  efexple  26774  bposlem5  26781  bposlem6  26782  bposlem7  26783  lgsdilem  26817  2lgslem1a2  26883  2sqreuop  26955  2sqreuopnn  26956  2sqreuoplt  26957  2sqreuopltb  26958  2sqreuopnnlt  26959  2sqreuopnnltb  26960  dchrisumlem3  26984  dchrmusumlema  26986  dchrmusum2  26987  dchrvmasumlem2  26991  dchrvmasumlema  26993  dchrvmasumiflem1  26994  dchrisum0flblem2  27002  dchrisum0flb  27003  dchrisum0lema  27007  dchrisum0lem1b  27008  dchrisum0lem2  27011  pntrlog2bndlem2  27071  pntibndlem2  27084  pntlemf  27098  ostth2lem1  27111  qabvle  27118  sltval2  27149  sltres  27155  nolesgn2o  27164  nogesgn1o  27166  nodense  27185  nolt02o  27188  nogt01o  27189  noresle  27190  nosupbnd2lem1  27208  nosupbnd2  27209  noinfbnd2lem1  27223  noinfbnd2  27224  addsproplem1  27443  addsprop  27450  sltadd2im  27459  sleadd2im  27461  sleadd1  27462  sleadd2  27463  sltadd1  27465  sltsub1  27533  sltsub2  27534  sltsubsubbd  27540  sltsubsub2bd  27541  posdifsd  27551  mulsproplemcbv  27561  mulsproplem1  27562  mulsprop  27576  slemuld  27584  sltmul1d  27615  sltmulneg1d  27618  sltmulneg2d  27619  legso  27840  iscgra  28050  isleag  28088  iseqlg  28108  brbtwn2  28153  axlowdim  28209  ewlksfval  28848  isnvlem  29851  nvtri  29911  nmlnoubi  30037  nmblolbii  30040  nmblolbi  30041  blocnilem  30045  sii  30095  ubthlem2  30112  minvecolem3  30117  minvecolem5  30122  minvecolem6  30123  norm-ii  30379  norm3dif  30391  norm3adifi  30394  bcs  30422  pjnorm  30965  pjnel  30967  nmbdoplbi  31265  nmbdoplb  31266  nmcoplb  31271  lnconi  31274  nmbdfnlb  31291  nmcfnlb  31295  pjdifnormi  31408  mdslmd2i  31571  cvmd  31577  cvexch  31615  cdj1i  31674  cdj3lem1  31675  cdj3lem2b  31678  cdj3lem3b  31681  cdj3i  31682  isoun  31911  ismnt  32141  mgcmntco  32152  dfmgc2lem  32153  dfmgc2  32154  mgcf1o  32161  isomnd  32207  omndadd  32212  omndmul  32220  ogrpinvlt  32229  gsumle  32230  isinftm  32315  xrmulc1cn  32899  lmdvg  32922  nexple  32996  faeval  33233  brfae  33235  inelcarsg  33299  carsgsigalem  33303  carsgclctunlem2  33307  carsgclctun  33309  hgt750lemc  33648  hgt750lemd  33649  hgt749d  33650  sconnpht  34209  snmlval  34311  satfv1lem  34342  satfv1  34343  satfv0fun  34351  satfv0fvfmla0  34393  lediv2aALT  34651  faclim  34705  fvtransport  34993  idinside  35045  btwnconn1lem7  35054  btwnconn1lem11  35058  btwnconn1lem12  35059  nn0prpwlem  35196  bj-opabco  36058  poimirlem29  36506  heicant  36512  itg2addnclem  36528  itg2addnclem3  36530  itg2gt0cn  36532  ftc1anclem6  36555  ftc1anc  36558  ftc2nc  36559  dvasin  36561  areacirclem1  36565  seqpo  36604  incsequz  36605  metf1o  36612  mettrifi  36614  cntotbnd  36653  heiborlem4  36671  heiborlem6  36673  heiborlem10  36677  bfplem1  36679  bfplem2  36680  isopos  38039  oplecon3b  38059  atlatle  38179  4at2  38474  pmaple  38621  islaut  38943  lautcnvle  38949  lautco  38957  ltrncnvel  39002  cdlemeg49lebilem  39399  cdlemg17h  39528  tendoset  39619  tendotp  39621  cdlemk39s  39799  lcmineqlem23  40905  lcmineqlem  40906  intlewftc  40915  aks4d1p1p4  40925  dvle2  40926  aks4d1p8d2  40939  aks4d1p9  40942  aks4d1  40943  2ap1caineq  40950  sticksstones1  40951  sticksstones2  40952  sticksstones3  40953  sticksstones8  40958  sticksstones10  40960  sticksstones11  40961  sticksstones12a  40962  sticksstones15  40966  factwoffsmonot  41012  brif12  41040  dvdsexpnn0  41228  dvdsexpb  41229  reltsub1  41256  irrapxlem2  41547  irrapxlem4  41549  irrapxlem5  41550  irrapxlem6  41551  pellexlem3  41555  monotuz  41666  monotoddzzfi  41667  monotoddzz  41668  jm2.17a  41685  jm2.17b  41686  rmygeid  41689  rmydioph  41739  expdiophlem1  41746  expdiophlem2  41747  ttac  41761  fnwe2lem2  41779  relexp01min  42450  cvgdvgrat  43058  monoords  43994  supxrgelem  44034  supxrge  44035  abslt2sqd  44057  ltmulneg  44089  ltdiv23neg  44091  monoordxrv  44179  monoordxr  44180  monoord2xrv  44181  monoord2xr  44182  evthiccabs  44196  sqrlearg  44253  climinf  44309  climinff  44314  limsupres  44408  climinf2  44410  climinf2mpt  44417  climinfmpt  44418  supcnvlimsup  44443  liminfval2  44471  liminflelimsuplem  44478  liminfltlem  44507  fprodsubrecnncnvlem  44610  fprodaddrecnncnvlem  44612  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  iblspltprt  44676  itgspltprt  44682  stoweidlem3  44706  fourierdlem2  44812  fourierdlem3  44813  fourierdlem11  44821  fourierdlem12  44822  fourierdlem15  44825  fourierdlem34  44844  fourierdlem41  44851  fourierdlem48  44857  fourierdlem49  44858  fourierdlem79  44888  fourierdlem83  44892  fourierdlem89  44898  fourierdlem91  44900  fourierdlem100  44909  fourierdlem107  44916  fourierdlem109  44918  fourierdlem112  44921  etransclem31  44968  etransclem32  44969  rrndistlt  44993  ioorrnopn  45008  ioorrnopnxrlem  45009  sge0less  45095  sge0le  45110  sge0split  45112  sge0lempt  45113  sge0iunmptlemre  45118  sge0isum  45130  sge0seq  45149  meaiuninclem  45183  meaiininclem  45189  meaiininc  45190  isome  45197  omeunile  45208  omeiunlempt  45223  carageniuncllem2  45225  0ome  45232  isomenndlem  45233  isomennd  45234  ovnssle  45264  ovnsubadd  45275  hsphoidmvle2  45288  hsphoidmvle  45289  hoidmvval0  45290  hoidmv1lelem1  45294  hoidmv1lelem2  45295  hoidmv1lelem3  45296  hoidmv1le  45297  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvlelem4  45301  hoidmvlelem5  45302  hoidmvle  45303  hoidifhspdmvle  45323  hspmbllem2  45330  hspmbl  45332  ovnsubadd2lem  45348  ovolval4lem2  45353  ovolval4  45354  ovolval5lem2  45356  vonioolem2  45384  vonioo  45385  vonicclem2  45387  vonicc  45388  smfid  45455  smflimlem3  45476  natglobalincr  45578  tworepnotupword  45587  2elfz2melfz  46013  smonoord  46026  iccpart  46071  iccpartimp  46072  iccpartres  46073  sqrtpwpw2p  46193  ismgmALT  46620  iscmgmALT  46621  issgrpALT  46622  iscsgrpALT  46623  lindslinindsimp2lem5  47097  rrx2plordisom  47363  aacllem  47802