Theorem breq12d 5085

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   class class class wbr 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073

This theorem is referenced by:  breq123d  5086  3brtr3d  5103  3brtr4d  5104  sbcbr  5127  pocl  5534  csbcnvgALT  5826  cnvpo  6238  sbcfung  6509  isoeq1  7261  isocnv  7274  isotr  7280  caovordig  7561  caovordg  7563  caovord2d  7565  caovord  7567  ofrfvalg  7628  ofrval  7632  ofrfval2  7641  caofref  7651  fnwelem  8071  poseq  8098  fundmeng  8969  enrefnn  8983  xpsneng  8990  xpcomeng  8997  xpdom2g  9001  limensuc  9082  infensuc  9083  pssnn  9093  unxpdom  9159  dif1ennnALT  9177  unfilem3  9207  fodomfi  9212  domunfican  9222  fodomfiOLD  9230  marypha1lem  9336  infsupprpr  9409  wemaplem1  9451  wemaplem2  9452  wemapwe  9609  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  dmttrcl  9633  rnttrcl  9634  ttrclselem2  9638  dif1card  9923  infxpenlem  9926  nnadju  10111  pwsdompw  10116  infmap2  10130  sornom  10190  isfin5  10212  isfin6  10213  domtriomlem  10355  axdc2lem  10361  axdclem2  10433  pwcfsdom  10497  cfpwsdom  10498  alephom  10499  fpwwe2lem6  10550  fpwwe2lem8  10552  tskcard  10695  ordpipq  10856  adderpqlem  10868  mulerpqlem  10869  mulcanenq  10874  lterpq  10884  ltanq  10885  ltmnq  10886  ltaddnq  10888  ltrnq  10893  archnq  10894  reclem4pr  10964  ltasr  11014  sqgt0sr  11020  axpre-ltadd  11081  axpre-mulgt0  11082  ltadd1  11608  leadd2  11610  ltmul2  11997  lemul2  11999  lemul1a  12000  ltdiv1  12011  ltdiv2  12033  lediv2  12037  div4p1lem1div2  12423  nn0ledivnn  13048  xleadd1  13198  xltadd2  13200  xsubge0  13204  xlemul1a  13231  xlemul1  13233  xlemul2  13234  xltmul2  13236  ltdifltdiv  13784  fzennn  13921  monoord  13985  monoord2  13986  expmordi  14120  ltexp2r  14126  leexp1a  14128  sqlecan  14162  bernneq  14182  faclbnd  14243  faclbnd3  14245  faclbnd4lem1  14246  faclbnd4lem2  14247  faclbnd4lem3  14248  faclbnd4lem4  14249  faclbnd6  14252  facubnd  14253  rlimcld2  15531  isercoll2  15622  climsup  15623  iseraltlem2  15636  fsumabs  15755  fsumrlim  15765  climcndslem1  15805  climcndslem2  15806  supcvg  15812  geomulcvg  15832  cvgrat  15839  ntrivcvgtail  15856  ruclem2  16190  ruclem8  16195  addmodlteqALT  16285  fproddvdsd  16295  sadcaddlem  16417  sadcadd  16418  nn0seqcvgd  16530  algcvg  16536  algcvga  16539  eucalgcvga  16546  isprm5  16668  qnumgt0  16711  pcprendvds2  16803  pcpremul  16805  pcadd2  16852  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  2expltfac  17054  xpsle  17534  mreexexlemd  17601  issubc  17793  latjlej2  18411  latmlem2  18427  ischn  18564  chnltm1  18566  chnind  18578  chnub  18579  sylow1lem3  19566  isslw  19574  fislw  19591  efgi  19685  lt6abl  19861  ablfac1eu  20041  isomnd  20089  omndadd  20094  omndmul  20101  ogrpinvlt  20110  gsumle  20111  isabv  20783  abvtri  20794  psdmul  22154  cayleyhamilton1  22875  isucn  24260  ispsmet  24287  psmettri2  24292  ismet  24306  isxmet  24307  xmettri2  24323  imasdsf1olem  24356  imasf1oxmet  24358  blvalps  24368  blval  24369  comet  24496  stdbdxmet  24498  nrmmetd  24557  tngngp  24637  tngngp3  24639  nmofval  24697  nmolb2d  24701  nmoi  24711  nmoix  24712  icopnfhmeo  24928  xrhmeo  24931  evth2  24945  pi1grplem  25034  minveclem6  25419  ovolfiniun  25486  ovoliunlem3  25489  voliunlem3  25537  ioombl1  25547  mbfmax  25634  mbfpos  25636  itg1climres  25699  mbfi1fseqlem2  25701  mbfi1fseqlem6  25705  mbfi1fseq  25706  mbfmullem  25710  itg2split  25734  itg2monolem1  25735  itg2monolem3  25737  itg2mono  25738  itg2i1fseqle  25739  itg2i1fseq  25740  itg2i1fseq2  25741  itg2addlem  25743  rolle  25975  dvlip  25978  c1lip1  25982  dvcnvrelem1  26002  dvcvx  26005  ply1divex  26120  q1pval  26138  fta1glem2  26152  fta1g  26153  fta1b  26155  plydivlem3  26279  fta1lem  26291  fta1  26292  aalioulem3  26318  aalioulem4  26319  aaliou3lem2  26327  aaliou3lem8  26329  aaliou3lem9  26334  ulmdvlem1  26383  ulmdvlem3  26385  abelthlem2  26415  abelthlem7a  26420  argrege0  26593  cxplt  26676  cxplea  26678  cxple2  26679  cxplt3  26682  logbleb  26765  logblt  26766  rlimcxp  26955  scvxcvx  26967  jensenlem2  26969  ftalem3  27056  ftalem7  27060  vmalelog  27186  chtub  27193  chpchtsum  27200  bclbnd  27261  efexple  27262  bposlem5  27269  bposlem6  27270  bposlem7  27271  lgsdilem  27305  2lgslem1a2  27371  2sqreuop  27443  2sqreuopnn  27444  2sqreuoplt  27445  2sqreuopltb  27446  2sqreuopnnlt  27447  2sqreuopnnltb  27448  dchrisumlem3  27472  dchrmusumlema  27474  dchrmusum2  27475  dchrvmasumlem2  27479  dchrvmasumlema  27481  dchrvmasumiflem1  27482  dchrisum0flblem2  27490  dchrisum0flb  27491  dchrisum0lema  27495  dchrisum0lem1b  27496  dchrisum0lem2  27499  pntrlog2bndlem2  27559  pntibndlem2  27572  pntlemf  27586  ostth2lem1  27599  qabvle  27606  ltsval2  27638  ltsres  27644  nolesgn2o  27653  nogesgn1o  27655  nodense  27674  nolt02o  27677  nogt01o  27678  noresle  27679  nosupbnd2lem1  27697  nosupbnd2  27698  noinfbnd2lem1  27712  noinfbnd2  27713  addsproplem1  27979  addsprop  27986  ltadds2im  27996  leadds2im  27998  leadds1  27999  leadds2  28000  ltadds1  28002  ltsubs1  28086  ltsubs2  28087  ltsubsubsbd  28093  ltsubsubs2bd  28094  posdifsd  28108  subsge0d  28110  mulsproplemcbv  28125  mulsproplem1  28126  mulsprop  28140  lemulsd  28148  ltmuls1d  28183  ltmulnegs1d  28186  ltmulnegs2d  28187  lemuls1ad  28192  zsoring  28419  pw2gt0divsd  28455  pw2ge0divsd  28456  legso  28685  iscgra  28895  isleag  28933  iseqlg  28953  brbtwn2  28992  axlowdim  29048  ewlksfval  29688  isnvlem  30699  nvtri  30759  nmlnoubi  30885  nmblolbii  30888  nmblolbi  30889  blocnilem  30893  sii  30943  ubthlem2  30960  minvecolem3  30965  minvecolem5  30970  minvecolem6  30971  norm-ii  31227  norm3dif  31239  norm3adifi  31242  bcs  31270  pjnorm  31813  pjnel  31815  nmbdoplbi  32113  nmbdoplb  32114  nmcoplb  32119  lnconi  32122  nmbdfnlb  32139  nmcfnlb  32143  pjdifnormi  32256  mdslmd2i  32419  cvmd  32425  cvexch  32463  cdj1i  32522  cdj3lem1  32523  cdj3lem2b  32526  cdj3lem3b  32529  cdj3i  32530  fnfvor  32701  ofrco  32702  isoun  32794  nexple  32936  ismnt  33062  mgcmntco  33073  dfmgc2lem  33074  dfmgc2  33075  mgcf1o  33082  isinftm  33262  rlocaddval  33349  rlocmulval  33350  fldext2chn  33912  constrextdg2lem  33932  constrext2chn  33943  xrmulc1cn  34114  lmdvg  34137  faeval  34430  brfae  34432  inelcarsg  34495  carsgsigalem  34499  carsgclctunlem2  34503  carsgclctun  34505  hgt750lemc  34831  hgt750lemd  34832  hgt749d  34833  fineqvnttrclse  35305  sconnpht  35457  snmlval  35559  satfv1lem  35590  satfv1  35591  satfv0fun  35599  satfv0fvfmla0  35641  lediv2aALT  35905  faclim  35974  fvtransport  36260  idinside  36312  btwnconn1lem7  36321  btwnconn1lem11  36325  btwnconn1lem12  36326  ditgeq123dv  36449  cbvditgdavw2  36526  nn0prpwlem  36550  weiunval  36690  weiunfrlem  36692  bj-opabco  37548  poimirlem29  38016  heicant  38022  itg2addnclem  38038  itg2addnclem3  38040  itg2gt0cn  38042  ftc1anclem6  38065  ftc1anc  38068  ftc2nc  38069  dvasin  38071  areacirclem1  38075  seqpo  38114  incsequz  38115  metf1o  38122  mettrifi  38124  cntotbnd  38163  heiborlem4  38181  heiborlem6  38183  heiborlem10  38187  bfplem1  38189  bfplem2  38190  isopos  39672  oplecon3b  39692  atlatle  39812  4at2  40106  pmaple  40253  islaut  40575  lautcnvle  40581  lautco  40589  ltrncnvel  40634  cdlemeg49lebilem  41031  cdlemg17h  41160  tendoset  41251  tendotp  41253  cdlemk39s  41431  lcmineqlem23  42536  lcmineqlem  42537  intlewftc  42546  aks4d1p1p4  42556  dvle2  42557  aks4d1p8d2  42570  aks4d1p9  42573  aks4d1  42574  2ap1caineq  42630  sticksstones1  42631  sticksstones2  42632  sticksstones3  42633  sticksstones8  42638  sticksstones10  42640  sticksstones11  42641  sticksstones12a  42642  sticksstones15  42646  aks6d1c7lem3  42667  unitscyglem1  42680  brif12  42712  dvdsexpnn0  42811  dvdsexpb  42812  reltsub1  42863  irrapxlem2  43268  irrapxlem4  43270  irrapxlem5  43271  irrapxlem6  43272  pellexlem3  43276  monotuz  43386  monotoddzzfi  43387  monotoddzz  43388  jm2.17a  43405  jm2.17b  43406  rmygeid  43409  rmydioph  43459  expdiophlem1  43466  expdiophlem2  43467  ttac  43481  fnwe2lem2  43496  relexp01min  44157  cvgdvgrat  44757  relpeq1  45388  monoords  45745  supxrgelem  45782  supxrge  45783  abslt2sqd  45805  ltmulneg  45836  ltdiv23neg  45838  monoordxrv  45924  monoordxr  45925  monoord2xrv  45926  monoord2xr  45927  evthiccabs  45941  sqrlearg  45998  climinf  46051  climinff  46056  limsupres  46148  climinf2  46150  climinf2mpt  46157  climinfmpt  46158  supcnvlimsup  46183  liminfval2  46211  liminfltlem  46247  fprodsubrecnncnvlem  46350  fprodaddrecnncnvlem  46352  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  iblspltprt  46416  itgspltprt  46422  stoweidlem3  46446  fourierdlem2  46552  fourierdlem3  46553  fourierdlem11  46561  fourierdlem12  46562  fourierdlem15  46565  fourierdlem34  46584  fourierdlem41  46591  fourierdlem48  46597  fourierdlem49  46598  fourierdlem79  46628  fourierdlem83  46632  fourierdlem89  46638  fourierdlem91  46640  fourierdlem100  46649  fourierdlem107  46656  fourierdlem109  46658  fourierdlem112  46661  etransclem31  46708  etransclem32  46709  rrndistlt  46733  ioorrnopn  46748  ioorrnopnxrlem  46749  sge0less  46835  sge0le  46850  sge0split  46852  sge0lempt  46853  sge0iunmptlemre  46858  sge0isum  46870  sge0seq  46889  meaiuninclem  46923  meaiininclem  46929  meaiininc  46930  isome  46937  omeunile  46948  omeiunlempt  46963  carageniuncllem2  46965  0ome  46972  isomenndlem  46973  isomennd  46974  ovnssle  47004  ovnsubadd  47015  hsphoidmvle2  47028  hsphoidmvle  47029  hoidmvval0  47030  hoidmv1lelem1  47034  hoidmv1lelem2  47035  hoidmv1lelem3  47036  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  hoidmvlelem5  47042  hoidmvle  47043  hoidifhspdmvle  47063  hspmbllem2  47070  hspmbl  47072  ovnsubadd2lem  47088  ovolval4lem2  47093  ovolval4  47094  ovolval5lem2  47096  vonioolem2  47124  vonioo  47125  vonicclem2  47127  vonicc  47128  smfid  47195  smflimlem3  47216  ormkglobd  47320  natglobalincr  47322  chnerlem1  47327  squeezedltsq  47333  2elfz2melfz  47781  smonoord  47840  iccpart  47891  iccpartimp  47892  iccpartres  47893  sqrtpwpw2p  48016  grlicsym  48504  grlictr  48506  ismgmALT  48714  iscmgmALT  48715  issgrpALT  48716  iscsgrpALT  48717  lindslinindsimp2lem5  48953  rrx2plordisom  49214  aacllem  50291